lift_mk — Mathlib

English

For any g ∈ G, the lifted map evaluated at the coset represented by g equals φ(g). More precisely, if π: G → G/N is the quotient map, then φ̂(π(g)) = φ(g).

Русский

Для любого элемента g ∈ G отображение лифта на косете, представляемом g, равно φ(g). То есть φ̂(π(g)) = φ(g) для всех g ∈ G.

LaTeX

$$$\\hat{\\varphi}(\\pi(g)) = \\varphi(g) \\quad (g \\in G).$$$

Lean4

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

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