subtypeVal — Mathlib

English

There is a Freiman-homomorphism from the universal set of a submonoid S to the ambient type via the inclusion map Subtype.val.

Русский

Существует Фриманова-гомоморфизм между универсуальным множеством подмоноида S и окружающим типом через включение Subtype.val.

LaTeX

$$$IsMulFreimanHom n (univ : Set s) univ Subtype.val$$$

Lean4

@[to_additive]
theorem subtypeVal {S : Type*} [SetLike S α] [SubmonoidClass S α] {s : S} :
    IsMulFreimanHom n (univ : Set s) univ Subtype.val :=
  MonoidHomClass.isMulFreimanHom (SubmonoidClass.subtype s) (mapsTo_univ ..)

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