Theorems · Theorem · general topology
ZMod.toAddCircle_injective
∀ (N : ℕ) [inst : NeZero N], Function.Injective ⇑ZMod.toAddCircle
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NeZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement and proof · cited by 25,697
- AddMonoidHomstatement · cited by 3,230
- zero_addproof · cited by 2,366
- LT.lt.ne'proof · cited by 1,417
- ZModstatement and proof · cited by 1,024
- AddSubgroup.zmultiplesstatement · cited by 493
- QuotientAddGroup.mkproof · cited by 348
- Nat.cast_nonneg'proof · cited by 245
- ZMod.valproof · cited by 159
- UnitAddCirclestatement and proof · cited by 157
- Nat.cast_posproof · cited by 113
Cited by3
Results whose statement or proof uses this declaration.
- ZMod.toAddCircle_eq_zeroproof · cited by 3
- ZMod.injective_toCircleproof · cited by 2
- ZMod.toAddCircle_injproof · cited by 0