integerSetTorsionSMul_stabilizer — Mathlib

English

The stabilizer of torsion acts trivially on integerSet: the stabilizer is the bottom subgroup.

Русский

Стабилизатор действия торов на integerSet совпадает с нулевой подгруппой.

LaTeX

$$$\\operatorname{integerSetTorsionSMul\\_stabilizer}(a) = \\{e\\}$$$

Lean4

theorem integerSetTorsionSMul_stabilizer (a : integerSet K) : MulAction.stabilizer (torsion K) a = ⊥ :=
  by
  refine (Subgroup.eq_bot_iff_forall _).mpr fun ζ hζ ↦ ?_
  rwa [MulAction.mem_stabilizer_iff, Subtype.ext_iff, integerSetTorsionSMul_smul_coe, unitSMul_smul, ←
    mixedEmbedding_preimageOfMemIntegerSet, ← map_mul, (mixedEmbedding_injective K).eq_iff, ← map_mul, ←
    RingOfIntegers.ext_iff, mul_eq_right₀, Units.val_eq_one, OneMemClass.coe_eq_one] at hζ
  exact nonZeroDivisors.coe_ne_zero _

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