subtype — Mathlib

English

There is a canonical inclusion map Subgroup.subtype: H →* G from a subgroup to the ambient group.

Русский

Существует каноническое вложение Subgroup.subtype: H →* G от подгруппы к группе.

LaTeX

$$$$ \\mathrm{SubgroupClass.subtype}(H) : H \\to^* G \\text{ is the canonical inclusion}. $$$$

Lean4

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

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