ker_mkMulHom_eq — Mathlib

English

The kernel of the quotient-map mkMulHom associated to a congruence c is exactly c itself: ker(mkMulHom c) = c.

Русский

Ядро отображения-кваритирования mkMulHom, связанного с конгруэнцией c, равняется самой конгруэнции: ker(mkMulHom c) = c.

LaTeX

$$$\ker (\,c.mkMulHom\,)= c$$$

Lean4

@[to_additive (attr := simp) /-- The kernel of the quotient map induced by an additive congruence
    relation `c` equals `c`. -/
    ]
theorem ker_mkMulHom_eq (c : Con M) : ker (mkMulHom c) = c :=
  ext fun _ _ => Quotient.eq''

Похожие утверждения