lift_quot_mk — Mathlib

English

The kernel of the descended map equals the image of ker φ under the quotient map mk' N.

Русский

Ядро спустившегося отображения равно образу ядра φ под отображением mk' N.

LaTeX

$$$\\ker(\\hat{\\varphi}) = \\operatorname{map} (\\mathrm{mk}' N) (\\ker \\varphi).$$$

Lean4

@[to_additive (attr := simp)]
theorem lift_quot_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (Quot.mk _ g :  Q ) = φ g :=
  rfl

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