Theorems · Theorem · group theory

Con.comap_conGen_of_bijective

∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M → N),
  Function.Bijective f →
    ∀ (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop),
      Con.comap f H (conGen rel) = conGen fun x y => rel (f x) (f y)

Defined in: Mathlib.GroupTheory.Congruence.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Mul Mul

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Function.Bijectivestatement and proof · cited by 863
Constatement · cited by 152
conGenstatement · cited by 23
Con.comapstatement · cited by 15
MulEquiv.ofBijectiveproof · cited by 5
Con.comap_conGen_equivproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.