smul_eq_of_le_smul — Mathlib

English

If in a finite group action on a poset X, a ≤ g • a holds, then g • a = a.

Русский

Пусть конечная группа действует на упорядоченное множество X; если a ≤ g·a, тогда g·a = a.

LaTeX

$$a ≤ g • a → g • a = a$$

Lean4

theorem smul_eq_of_le_smul {G : Type*} [Group G] [Finite G] {α : Type*} [PartialOrder α] {g : G} {a : α} [MulAction G α]
    [CovariantClass G α HSMul.hSMul LE.le] (h : a ≤ g • a) : g • a = a :=
  by
  have key := smul_mono_right g (le_pow_smul h (Nat.card G - 1))
  rw [smul_smul, ← _root_.pow_succ', Nat.sub_one_add_one_eq_of_pos Nat.card_pos, pow_card_eq_one', one_smul] at key
  exact le_antisymm key h

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