subgroupOf — Mathlib

English

For subgroups H, K of G, the intersection H ∧ K, viewed as a subgroup of K, is the subgroup H ∩ K of K.

Русский

Для подгрупп H и K группы G пересечение H ∩ K, рассматриваемое как подгруппа K, является подгруппой H ∩ K внутри K.

LaTeX

$$$ (H \\cap K) \\text{ considered as a subgroup of } K \\; = \\; H \\cap K $$$

Lean4

/-- For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`. -/
@[to_additive /-- For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`. -/
    ]
def subgroupOf (H K : Subgroup G) : Subgroup K :=
  H.comap K.subtype

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