Theorems · Definition · number theory
ZMod.ringEquivCongr
{m n : ℕ} → m = n → ZMod m ≃+* ZMod nThe identity between ZMod m and ZMod n when m = n, as a ring isomorphism.
- Defined in
- Mathlib.Data.ZMod.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Quot.sound
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.
- Equivproof · cited by 8,337
- RingEquivstatement · cited by 1,147
- ZModstatement and proof · cited by 1,024
- finCongrproof · cited by 78
- RingEquiv.reflproof · cited by 72
Cited by13
Results whose statement or proof uses this declaration.
- modularCyclotomicCharacterproof · cited by 6
- ZMod.ringEquivCongr_valstatement and proof · cited by 3
- AddCommGroup.equiv_free_prod_directSum_zmodproof · cited by 2
- cyclotomicCharacter.toZModPow_toFunproof · cited by 2
- ZMod.ringEquivCongr_reflstatement and proof · cited by 1
- ZMod.ringEquivCongr_symmstatement and proof · cited by 1
- ZMod.ringEquivCongr_transstatement and proof · cited by 1
- modularCyclotomicCharacter.uniqueproof · cited by 1
- ZMod.ringEquivCongr_intCaststatement and proof · cited by 0
- ZMod.ringEquivCongr_refl_applystatement · cited by 0
- ZMod.ringEquivCongr_ringEquivCongr_applystatement and proof · cited by 0
- ZMod.ringEquivCongr.congr_simpstatement and proof · cited by 0