stabilizer_smul_eq_left — Mathlib

English

Suppose the map x ↦ x • b is injective (IsScalarTower). Then the stabilizer of a and of a • b coincide: Stab_G(a • b) = Stab_G(a).

Русский

Пусть отображение x ↦ x • b инъективно (IsScalarTower). Тогда стабилизатор a и стабилизатор a • b совпадают: Stab_G(a • b) = Stab_G(a).

LaTeX

$$\big(\operatorname{Injective}(\lambda x. x \cdot b)\big) \Rightarrow \operatorname{Stab}_G(a \cdot b) = \operatorname{Stab}_G(a)$$

Lean4

@[to_additive (attr := simp)]
theorem stabilizer_smul_eq_left [SMul α β] [IsScalarTower G α β] (a : α) (b : β) (h : Injective (· • b : α → β)) :
    stabilizer G (a • b) = stabilizer G a :=
  by
  refine (le_stabilizer_smul_left _ _).antisymm' fun a ha ↦ ?_
  simpa only [mem_stabilizer_iff, ← smul_assoc, h.eq_iff] using ha

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