zero_zpow
theorem zero_zpow : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (z : ℤ), z ≠ 0 → 0 ^ z = 0
This theorem, `zero_zpow`, states that for all integers `z` that are not equal to zero, zero raised to the power of `z` is equal to zero. Here, `G₀` is any type that forms a group with zero, which means it satisfies certain mathematical properties such as associativity and the existence of a zero element.
More concisely: For any non-zero integer `z` in a group `G₀` with identity element 0, 0 raised to the power of `z` equals 0.
|
zpow_ne_zero_of_ne_zero
theorem zpow_ne_zero_of_ne_zero : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (z : ℤ), a ^ z ≠ 0
This theorem states that for any type `G₀` that has a structure of group with zero (i.e., it has both a group and field structure with a designated zero element that behaves as the additive identity), if `a` is an element of `G₀` that is not zero, then raising `a` to any integer power `z` will also not result in zero. In other words, a non-zero element remains non-zero when raised to any integer power in a group with zero.
More concisely: If `G₀` is a group with zero and `a` is a non-zero element in `G₀`, then for all integers `z`, `a^z ≠ 0`.
|
zpow_ne_zero
theorem zpow_ne_zero : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {x : G₀} (n : ℤ), x ≠ 0 → x ^ n ≠ 0
This theorem states that for any GroupWithZero `G₀` and any element `x` of `G₀`, if `x` is not equal to zero then `x` raised to any integer `n` is also not equal to zero. The GroupWithZero typeclass in Lean 4 is used to represent groups that have an additional distinguished element that serves as a zero and satisfies the property that any element times zero equals zero.
More concisely: If `G₀` is a group with zero and `x` is a non-zero element in `G₀`, then `x^n` is also non-zero for any integer `n`.
|
pow_sub₀
theorem pow_sub₀ :
∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) {m n : ℕ}, a ≠ 0 → n ≤ m → a ^ (m - n) = a ^ m * (a ^ n)⁻¹
This theorem states that for any type `G₀` that forms a group with zero, and for any element `a` of type `G₀` and natural numbers `m` and `n` such that `a` is not zero and `n` is less than or equal to `m`, the power of `a` to the difference of `m` and `n` (`m - n`) equals to the product of the power of `a` to `m` and the inverse of the power of `a` to `n` (`a ^ m * (a ^ n)⁻¹`). This theorem essentially expresses the basic property of exponents in the context of groups.
More concisely: For any group `G₀` with identity `0`, and for all `a ≠ 0` in `G₀` and natural numbers `m ≥ n`, `a ^ (m - n) = a ^ m * (a ^ n)⁻¹`.
|
Commute.zpow_right₀
theorem Commute.zpow_right₀ :
∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a b : G₀}, Commute a b → ∀ (m : ℤ), Commute a (b ^ m)
This theorem states that for any two elements `a` and `b` of a group with zero (`G₀`), if `a` and `b` commute (i.e., `a * b = b * a`), then `a` commutes with any integer power of `b` (i.e., `a * b^m = b^m * a` for any integer `m`). In other words, the commutativity property is preserved under exponentiation with an integer.
More concisely: If `a` and `b` are elements of a group with zero that commute, then `a` commutes with any integer power of `b`. In other words, `a * b^m = b^m * a` for all integers `m`.
|
zpow_add_one₀
theorem zpow_add_one₀ :
∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (n : ℤ), a ^ (n + 1) = a ^ n * a
This theorem states that for any non-zero element 'a' of a type 'G₀' that forms a group with zero, and for any integer 'n', the 'n+1'-th power of 'a' is equal to the 'n'-th power of 'a' multiplied by 'a'. Essentially, this is the power rule for multiplication applied to groups with zero.
More concisely: For any group element `a` in `G₀` different from zero and any integer `n`, the `(n + 1)`-th power of `a` equals the `n`-th power of `a` multiplied by `a`. In Lean notation: `(a ^ (n + 1)) = a ^ n * a`.
|
zpow_sub₀
theorem zpow_sub₀ :
∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (z1 z2 : ℤ), a ^ (z1 - z2) = a ^ z1 / a ^ z2 := by
sorry
This theorem states that for any non-zero element 'a' of a group with zero (a type 'G₀'), for any two integers 'z1' and 'z2', the exponentiation of 'a' to the power of the difference of 'z1' and 'z2' is equal to the division of 'a' to the power of 'z1' by 'a' to the power of 'z2'. In mathematical terms, it says that `a^(z1 - z2) = a^z1 / a^z2`, given that 'a' is not zero.
More concisely: For any non-zero element 'a' in a group and integers 'z1' and 'z2', the power 'a^(z1 - z2)' equals the quotient 'a^z1 / a^z2'.
|
zpow_add₀
theorem zpow_add₀ :
∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (m n : ℤ), a ^ (m + n) = a ^ m * a ^ n
This theorem states that for any type `G₀` that has a group with zero structure, given any element `a` of this type that is not zero, for any two integers `m` and `n`, the power of `a` to the sum of `m` and `n` is equal to the product of `a` to the power of `m` and `a` to the power of `n`. This is effectively stating the rule of indices for exponents: $a^{m+n} = a^m \cdot a^n$, in the setting of a group with zero.
More concisely: In a group with zero, the power of a non-zero element equals the product of its powers with respect to individual exponents. ($(a^{m+n})=(a^m)\cdot(a^n)$)
|