val_pow_le — Mathlib

English

For a ∈ ZMod n with 1 < n, the inequality (a^m).val ≤ a.val^m holds for all m.

Русский

Для a ∈ ZMod n при 1 < n выполняется неравенство (a^m).val ≤ a.val^m для любого m.

LaTeX

$$$ (a^m).val \le a.val^m $$$

Lean4

theorem val_pow_le {m n : ℕ} [Fact (1 < n)] {a : ZMod n} : (a ^ m).val ≤ a.val ^ m := by
  induction m with
  | zero => simp [ZMod.val_one]
  | succ m ih =>
    rw [pow_succ, pow_succ]
    apply le_trans (ZMod.val_mul_le _ _)
    apply Nat.mul_le_mul_right _ ih

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