English
If B is a block for a subgroup H, then for any g, the conjugate action yields a block for the conjugate subgroup H^g.
Русский
Если B — блок для подгруппы H, то для любого g получаем блок для сопряжённой подгруппы H^g.
LaTeX
$$IsBlock(G, B) ⇒ IsBlock((H.map (MulAut.conj g).toMonoidHom), g•B)$$
Lean4
/-- See `MulAction.isBlock_subgroup` for a version that works for the left action of a group on
itself. -/
@[to_additive /-- See `AddAction.isBlock_subgroup` for a version that works for the left 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 [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc, op_smul_coe_set hd]
