English
If B is a block for a subgroup S acting on H, then under scalar extension this yields a block for the conjugate subgroup and the same set B under smul.
Русский
Если B — блок для подгруппы S, действующей на H, то после сопряжения образуется блок для сопряжённой подгруппы и для того же множества под действием умножения.
LaTeX
$$IsBlock G (s : Set H) := ...$$
Lean4
/-- The orbit of `a` under a subgroup containing the stabilizer of `a` is a block -/
@[to_additive /-- The orbit of `a` under a subgroup containing the stabilizer of `a` is a block -/
]
theorem of_orbit {H : Subgroup G} {a : X} (hH : stabilizer G a ≤ H) : IsBlock G (MulAction.orbit H a) :=
by
rw [isBlock_iff_smul_eq_of_nonempty]
rintro g ⟨-, ⟨-, ⟨h₁, rfl⟩, h⟩, h₂, rfl⟩
suffices g ∈ H by rw [← Subgroup.coe_mk H g this, ← H.toSubmonoid.smul_def, smul_orbit (⟨g, this⟩ : H) a]
rw [← mul_mem_cancel_left h₂⁻¹.2, ← mul_mem_cancel_right h₁.2]
apply hH
simpa only [mem_stabilizer_iff, InvMemClass.coe_inv, mul_smul, inv_smul_eq_iff]
