isBlock_subgroup — Mathlib

English

If B is a block for H, then g • B is a block for the conjugate subgroup H^g.

Русский

Если B — блок для H, то g • B — блок для сопряжённой подгруппы H^g.

LaTeX

$$$IsBlock(H,B) \\Rightarrow IsBlock(H^{g}, g\\cdot B)$$$

Lean4

/-- See `MulAction.isBlock_subgroup'` for a version that works for the right action of a group on
itself. -/
@[to_additive /-- See `AddAction.isBlock_subgroup'` for a version that works for the right action
    of a group on itself. -/
    ]
theorem isBlock_subgroup : IsBlock G (s : Set H) :=
  by
  simp only [IsBlock, disjoint_left]
  rintro a b hab _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩
  refine hab ?_
  rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd]

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