translate — Mathlib

English

The additive version: translating a block by g via the additive action preserves the block property: AddAction.IsBlock.translate.

Русский

Аддитивная версия: перенос блока на величину g по аддитивному действию сохраняет свойство блока.

LaTeX

$$IsBlock(G,B) \\Rightarrow IsBlock(G,B+ g)$$

Lean4

/-- A translate of a block is a block -/
@[to_additive existing]
theorem translate (g : G) (hB : IsBlock G B) : IsBlock G (g • B) :=
  by
  rw [← isBlock_top] at hB ⊢
  rw [← Subgroup.map_comap_eq_self_of_surjective (G := G) (f := MulAut.conj g) (MulAut.conj g).surjective ⊤]
  apply IsBlock.of_subgroup_of_conjugate
  rwa [Subgroup.comap_top]

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