Theorems · Definition · group theory
powMonoidWithZeroHom
{M₀ : Type u_6} → [inst : CommMonoidWithZero M₀] → {n : ℕ} → n ≠ 0 → M₀ →*₀ M₀We define x ↦ x^n (for positive n : ℕ) as a MonoidWithZeroHom
- Defined in
- Mathlib.Algebra.GroupWithZero.Hom
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext
- Assumes
- CommMonoidWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MonoidHomproof · cited by 3,629
- CommMonoidWithZerostatement and proof · cited by 913
- MonoidWithZeroHomstatement · cited by 704
- OneHom.toFunproof · cited by 132
- MonoidHom.toOneHomproof · cited by 132
- powMonoidHomproof · cited by 35
Cited by2
Results whose statement or proof uses this declaration.
- powMonoidWithZeroHom_applystatement · cited by 0
- coe_powMonoidWithZeroHomstatement · cited by 0