subtype — Mathlib

English

The inclusion map from a subgroup H contained in K to K is a monoid homomorphism.

Русский

Включение подгруппы H в K является гомоморфизмом моноида.

LaTeX

$$$\text{inclusion} : H \to K \text{ is a monoid homomorphism with } \text{inclusion}(h)=h$$$

Lean4

/-- The natural group hom from a subgroup of group `G` to `G`. -/
@[to_additive /-- The natural group hom from an `AddSubgroup` of `AddGroup` `G` to `G`. -/
    ]
protected def subtype : H →* G where toFun := ((↑) : H → G); map_one' := rfl; map_mul' _ _ := rfl

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