Theorems · Theorem · general topology
ZMod.toAddCircle_eq_zero
∀ {N : ℕ} [inst : NeZero N] {j : ZMod N}, ZMod.toAddCircle j = 0 ↔ j = 0- Cited by
- 3 results in Mathlib
- Foundations
- Depth 116 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.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Realstatement · cited by 25,697
- AddMonoidHomstatement · cited by 3,230
- ZModstatement and proof · cited by 1,024
- AddSubgroup.zmultiplesstatement · cited by 493
- UnitAddCirclestatement · cited by 157
- map_eq_zero_iffproof · cited by 62
- ZMod.toAddCirclestatement and proof · cited by 32
- ZMod.toAddCircle_injectiveproof · cited by 3
Cited by3
Results whose statement or proof uses this declaration.
- ZMod.LFunction_stdAddChar_eq_expZetaproof · cited by 1
- ZMod.LFunction_eq_completed_div_gammaFactor_evenproof · cited by 1
- ZMod.LFunction_one_subproof · cited by 0