Theorems · Theorem · group theory
IsAddCyclic.ext
∀ {G : Type u_2} [inst : AddGroup G] [Finite G] [IsAddCyclic G] {d : ℕ} {a b : ZMod d},
Nat.card G = d → (∀ (t : G), a.val • t = b.val • t) → a = b- Cited by
- 0 results in Mathlib
- Foundations
- Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddGroupFiniteIsAddCyclic
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- Finitestatement and proof · cited by 3,029
- ZModstatement and proof · cited by 1,024
- Nat.cardstatement and proof · cited by 844
- AddSubgroup.zmultiplesproof · cited by 493
- Nat.ModEqproof · cited by 225
- ZMod.valstatement and proof · cited by 159
- IsAddCyclicstatement and proof · cited by 55
- ZMod.natCast_valproof · cited by 27
- ZMod.natCast_eq_natCast_iffproof · cited by 13
- ZMod.cast_id'proof · cited by 10
- IsAddCyclic.exists_generatorproof · cited by 8
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.