instSubgroupClass — Mathlib

English

Inclusion preserves composition: inclusion hKL ∘ inclusion hHK = inclusion (hHK.trans hKL).

Русский

Включение сохраняет композицию: inclusion hKL ∘ inclusion hHK = inclusion (hHK.trans hKL).

LaTeX

$$$$ inclusion(hKL) \\circ inclusion(hHK) = inclusion(hHK \\text{.trans} hKL). $$$$

Lean4

@[to_additive]
instance : SubgroupClass (Subgroup G) G where
  inv_mem := Subgroup.inv_mem' _
  one_mem _ := (Subgroup.toSubmonoid _).one_mem'
  mul_mem := (Subgroup.toSubmonoid _).mul_mem'

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