pullback_nonzero
theorem pullback_nonzero :
∀ {M₀ : Type u_1} {M₀' : Type u_2} [inst : MulZeroOneClass M₀] [inst_1 : Nontrivial M₀] [inst_2 : Zero M₀']
[inst_3 : One M₀'] (f : M₀' → M₀), f 0 = 0 → f 1 = 1 → Nontrivial M₀'
The theorem `pullback_nonzero` states that for any two types `M₀` and `M₀'`, if `M₀` is a MulZeroOneClass and is nontrivial, and `M₀'` is equipped with both zero and one, and there is a function `f` from `M₀'` to `M₀` such that `f` maps `0` to `0` and `1` to `1`, then `M₀'` is nontrivial. In other words, the nontrivial property can be pulled back along a function that preserves `0` and `1`.
More concisely: If `f` is a function from a nontrivial MulZeroOneClass `M′0` to a nontrivial MulZeroOneClass `M₀` with `f(0) = 0` and `f(1) = 1`, then `M′0` is nontrivial.
|
inv_mul_cancel
theorem inv_mul_cancel : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a⁻¹ * a = 1
This theorem states that for any type `G₀` that has a `GroupWithZero` structure, if we take any element `a` from `G₀` that is not equal to zero, the product of the inverse of `a` and `a` itself is equal to one. Here, `GroupWithZero` is a structure in Lean which represents a group with an additional element, zero, which has its own special properties, and `a⁻¹` denotes the multiplicative inverse of `a`. This theorem is essentially a formal statement of the fundamental property of multiplicative inverses in a group.
More concisely: For any group with zero `G₀` and non-zero element `a` in `G₀`, `a * a⁻¹ = 1`.
|
inv_ne_zero
theorem inv_ne_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a⁻¹ ≠ 0
This theorem states that for any type `G₀` that forms a group with an identity element zero, the inverse of any non-zero element `a` from `G₀` is also non-zero. In mathematical terms, if `a` belongs to a group with zero and `a` is not equal to zero, then the inverse of `a` (`a⁻¹`) is not equal to zero.
More concisely: In a group with identity element zero, the inverse of a non-zero element is also non-zero.
|