lift_comp_mk' — Mathlib

English

The lift composed with mk' equals the original homomorphism; i.e., the quotient lift agrees with φ on canonical representatives.

Русский

Композиция lift с mk' равна исходному гомоморфизму; то есть лифтинг через фактор-группу совпадает с φ на канонических представителях.

LaTeX

$$$(\\text{lift } N \\varphi HN) \\circ (\\mathrm{mk}' N) = \\varphi.$$$

Lean4

@[to_additive (attr := simp)]
theorem lift_comp_mk' (φ : G →* M) (HN : N ≤ φ.ker) : (QuotientGroup.lift N φ HN).comp (QuotientGroup.mk' N) = φ :=
  rfl

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