isUnit_comp — Mathlib

English

For every S and any j: N →* P, the image j∘f is unit on S, i.e., j(f(y)) is a unit for all y ∈ S.

Русский

Для любого S и гомоморфизма j: N →* P образ j∘f отображает элементы S в единицы, то есть j(f(y)) является единицей для каждого y ∈ S.

LaTeX

$$$ \forall y \in S,\ IsUnit(j(f(y))) $$$

Lean4

@[to_additive]
theorem isUnit_comp (j : N →* P) (y : S) : IsUnit (j.comp f.toMonoidHom y) :=
  ⟨Units.map j <| IsUnit.liftRight (f.restrict S) f.map_units y,
    show j _ = j _ from congr_arg j <| IsUnit.coe_liftRight (f.restrict S) f.map_units _⟩

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