subgroup — Mathlib

English

For every subgroup H, if B is a G-block, then B is an H-block.

Русский

Для каждой подгруппы H, если B — G-блок, то B — H-блок.

LaTeX

$$$\forall H \le G,\ IsBlock(H,B).$$$

Lean4

/-- If `B` is a `G`-block, then it is also a `H`-block for any subgroup `H` of `G`. -/
@[to_additive /-- If `B` is a `G`-block, then it is also a `H`-block for any subgroup `H` of `G`. -/
    ]
theorem subgroup {H : Subgroup G} (hB : IsBlock G B) : IsBlock H B := fun _ _ h ↦ hB h

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