Theorems · Definition · group theory

Con.comap

{M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] → [inst_1 : Mul N] → (f : M → N) → (∀ (x y : M), f (x * y) = f x * f y) → Con N → Con M

Given types with multiplications M, N and a congruence relation c on N, a multiplication-preserving map f : M → N induces a congruence relation on f's domain defined by 'x ≈ y iff f(x) is related to f(y) by c.'

Defined in

Mathlib.GroupTheory.Congruence.Defs

Cited by

15 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

MulMul