mul_ker_mk_eq — Mathlib

English

The kernel of the quotient map induced by a congruence c on M is precisely c.

Русский

Ядро отображения, порождаемого конгруэнцией c на M, точно равно c.

LaTeX

$$$\ker (\,c.mk') = c$$$

Lean4

/-- The kernel of the quotient map induced by a congruence relation `c` equals `c`. -/
@[to_additive (attr := simp) /-- The kernel of the quotient map induced by an additive congruence
    relation `c` equals `c`. -/
    ]
theorem mul_ker_mk_eq {c : Con M} : (mulKer ((↑) : M → c.Quotient) fun _ _ => rfl) = c :=
  ext fun _ _ => Quotient.eq''

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