smul_eq_of_smul_le — Mathlib

English

If g • a ≤ a holds under the same hypotheses, then g • a = a.

Русский

Если выполняется g•a ≤ a, то g•a = a.

LaTeX

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

Lean4

theorem smul_eq_of_smul_le {G : Type*} [Group G] [Finite G] {α : Type*} [PartialOrder α] {g : G} {a : α} [MulAction G α]
    [CovariantClass G α HSMul.hSMul LE.le] (h : g • a ≤ a) : g • a = a :=
  by
  have key := smul_mono_right g (pow_smul_le 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 h key

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