Theorems · Definition · group theory
Con.congr
{M : Type u_1} →
{N : Type u_2} →
[inst : Mul M] →
[inst_1 : Mul N] → {c : Con M} → {d : Con N} → (e : M ≃* N) → c = Con.comap ⇑e ⋯ d → c.Quotient ≃* d.QuotientA multiplicative equivalence e : α ≃* β generates an equivalence between quotient spaces,
if it is compatible with the relations.
- Defined in
- Mathlib.GroupTheory.Congruence.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- Equivproof · cited by 8,337
- MulEquivstatement and proof · cited by 1,142
- map_mulstatement · cited by 1,137
- Constatement and proof · cited by 152
- EquivLike.toEquivproof · cited by 125
- Con.Quotientstatement · cited by 48
- Con.toSetoidproof · cited by 38
- Con.comapstatement and proof · cited by 15
- Quotient.congrproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- Con.comapQuotientEquivOfSurjproof · cited by 3
- Con.congr_mkstatement · cited by 0
- Con.congr_symmstatement · cited by 0
- Con.comapQuotientEquivproof · cited by 0