Power operations on monoids with zero, semirings, and rings

This file provides additional lemmas about the natural power operator on rings and semirings. Further lemmas about ordered semirings and rings can be found in Algebra.GroupPower.Order.

def powMonoidWithZeroHom {M : Type u_3} [CommMonoidWithZero M] {n : ℕ} (hn : n ≠ 0) : M →*₀ M

We define x ↦ x^n (for positive n : ℕ) as a MonoidWithZeroHom

Equations

• powMonoidWithZeroHom hn = let __src := powMonoidHom n; { toFun := (↑__src).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem coe_powMonoidWithZeroHom {M : Type u_3} [CommMonoidWithZero M] {n : ℕ} (hn : n ≠ 0) : ⇑(powMonoidWithZeroHom hn) = fun (x : M) => x ^ n

@[simp]

theorem powMonoidWithZeroHom_apply {M : Type u_3} [CommMonoidWithZero M] {n : ℕ} (hn : n ≠ 0) (a : M) : (powMonoidWithZeroHom hn) a = a ^ n

theorem pow_dvd_pow_iff {R : Type u_1} [CancelCommMonoidWithZero R] {x : R} {n : ℕ} {m : ℕ} (h0 : x ≠ 0) (h1 : ¬IsUnit x) : x ^ n ∣ x ^ m ↔ n ≤ m