val_mul_le — Mathlib

English

For any a,b ∈ ZMod n, the representative of the product is not larger than the product of the representatives: (a*b).val ≤ a.val * b.val.

Русский

Для любых a,b ∈ ZMod n произведение имеет представителя, не превосходящий произведение представителей: (a*b).val ≤ a.val · b.val.

LaTeX

$$$ (a\cdot b).val \le a.val \cdot b.val $$$

Lean4

theorem val_mul_le {n : ℕ} (a b : ZMod n) : (a * b).val ≤ a.val * b.val :=
  by
  rw [val_mul]
  apply Nat.mod_le

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