val_mul_iff_lt — Mathlib

English

For all a,b ∈ ZMod n, the equality (a*b).val = a.val*b.val holds exactly when a.val*b.val < n.

Русский

Для любых a,b ∈ ZMod n равенство (a*b).val = a.val·b.val происходит тогда, когда a.val·b.val < n.

LaTeX

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

Lean4

theorem val_mul_iff_lt {n : ℕ} [NeZero n] (a b : ZMod n) : (a * b).val = a.val * b.val ↔ a.val * b.val < n :=
  by
  constructor <;> intro h
  · rw [← h]; apply ZMod.val_lt
  · apply ZMod.val_mul_of_lt h

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