val_mul_of_lt — Mathlib

English

If the product of the canonical representatives satisfies a.val * b.val < n, then the value of the product equals that product: (a*b).val = a.val * b.val.

Русский

Если произведение канонических представителей удовлетворяет a.val · b.val < n, тогда значение произведения равно этому произведению: (a*b).val = a.val · b.val.

LaTeX

$$$ a.val \cdot b.val < n \Rightarrow (a\cdot b).val = a.val \cdot b.val $$$

Lean4

theorem val_mul_of_lt {n : ℕ} {a b : ZMod n} (h : a.val * b.val < n) : (a * b).val = a.val * b.val :=
  by
  rw [val_mul]
  apply Nat.mod_eq_of_lt h

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