stabilizer_units_eq_bot_of_ne_zero

English

If x ≠ 0 in a module over R, then the stabilizer of x under the action of units of R is the bottom subgroup.

Русский

Если x не ноль в модуле над кольцом R, то стабилизатор x под действием единиц R равен нижней грани.

LaTeX

$$$x \\ne 0 \\Rightarrow \\mathrm{stabilizer}_{R^{\\times}}(x) = \\{1\\}$$$

Lean4

theorem stabilizer_units_eq_bot_of_ne_zero {x : M} (hx : x ≠ 0) : MulAction.stabilizer Rˣ x = ⊥ :=
  by
  rw [eq_bot_iff]
  intro g (hg : g.val • x = x)
  ext
  rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]

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