Theorems · Theorem · group theory
Con.comap_conGen_equiv
∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N) (rel : N → N → Prop),
Con.comap ⇑f ⋯ (conGen rel) = conGen fun x y => rel (f x) (f y)- Defined in
- Mathlib.GroupTheory.Congruence.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- DFunLike.coestatement and proof · cited by 62,936
- le_antisymmproof · cited by 2,068
- MulEquivstatement and proof · cited by 1,142
- map_mulstatement and proof · cited by 1,137
- MulEquiv.symmproof · cited by 482
- Constatement · cited by 152
- MulEquiv.surjectiveproof · cited by 41
- MulEquiv.apply_symm_applyproof · cited by 37
- MulEquiv.injectiveproof · cited by 36
- conGenstatement and proof · cited by 23
- Con.comapstatement and proof · cited by 15
- ConGen.Relproof · cited by 4
Cited by1
Results whose statement or proof uses this declaration.
- Con.comap_conGen_of_bijectiveproof · cited by 0