Theorems · Theorem · group theory
addOrderOf_zero
∀ {G : Type u_1} [inst : AddMonoid G], addOrderOf 0 = 1- Defined in
- Mathlib.GroupTheory.OrderOfElement
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement and proof · cited by 2,864
- addOrderOfstatement · cited by 208
- Function.minimalPeriodproof · cited by 100
- Function.minimalPeriod_idproof · cited by 2
- zero_add_eq_idproof · cited by 1
Cited by8
Results whose statement or proof uses this declaration.
- Nat.Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponentproof · cited by 1
- ZMod.addOrderOf_coeproof · cited by 1
- AddMonoid.exists_addOrderOf_eq_exponentproof · cited by 1
- add_notMem_of_addOrderOf_eq_twoproof · cited by 1
- AddMonoid.exponent_eq_prime_iffproof · cited by 1
- IsAddTorsionFree.addOrderOf_nonposproof · cited by 0
- addOrderOf_eq_two_iffproof · cited by 0
- IsAddUnit.addOrderOf_eq_zeroproof · cited by 0