Basic lemmas on monoids and groups with zero

In a reduced commutative monoid with zero, powers can be cancelled from annihilation relations: if a * b ^ k = 0, then a * b = 0. In a group with zero, integer powers of an n-th root of unity depend only on the exponent modulo n.

Main results

• TauCeti.mul_eq_zero_of_mul_pow_eq_zero: in a reduced commutative monoid with zero, a * b ^ k = 0 implies a * b = 0.
• TauCeti.zpow_eq_zpow_of_modEq: in a group with zero, if η ^ n = 1 and l ≡ m [ZMOD n], then η ^ l = η ^ m.

theorem TauCeti.mul_eq_zero_of_mul_pow_eq_zero {M : Type u_1} [CommMonoidWithZero M] [IsReduced M] {a b : M} {k : ℕ} (h : a * b ^ k = 0) : a * b = 0

In a reduced commutative monoid with zero, if a kills b ^ k then a kills b.

theorem TauCeti.zpow_eq_zpow_of_modEq {G₀ : Type u_1} [GroupWithZero G₀] {n : ℕ} {η : G₀} (hη : η ^ n = 1) {l m : ℤ} (h : l ≡ m [ZMOD ↑n]) : η ^ l = η ^ m

In a group with zero, powers of an n-th root of unity with exponents congruent modulo n agree.