coe_toHomUnits — Mathlib

English

For any f : G →* M and any g ∈ G, the underlying element of f.toHomUnits g equals f g, i.e. the unit-valued lift agrees with f on the level of M.

Русский

Для любого f : G →* M и любого g ∈ G соответствующий элемент в f.toHomUnits g равен f g, то есть переход в единицы сохраняет базовую карту.

LaTeX

$$$\\bigl(f^{\\mathrm{toHomUnits}}(g)\\bigr)_{\\text{val}} = f(g),$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_toHomUnits (f : G →* M) (g : G) : (f.toHomUnits g : M) = f g :=
  rfl

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