Theorems · Theorem · group theory

Con.comap_comp

∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (c : Con P) (g : N → P)
  (f : M → N) (hg : ∀ (x y : N), g (x * y) = g x * g y) (hf : ∀ (x y : M), f (x * y) = f x * f y),
  Con.comap (g ∘ f) ⋯ c = Con.comap f hf (Con.comap g hg c)

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites2

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

Constatement and proof · cited by 152
Con.comapstatement · cited by 15

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.