val_mul — Mathlib

English

Let n ∈ ℕ and a,b ∈ ZMod n. Then the canonical integer representing the product equals the product of the canonical integers modulo n: (a · b).val = (a.val · b.val) mod n.

Русский

Пусть n ∈ ℕ и a,b ∈ ZMod n. Тогда канонический представитель произведения равен произведению представителей по модулю n: (a · b).val ≡ a.val · b.val (mod n).

LaTeX

$$$ (a\cdot b).val = (a.val \cdot b.val) \\bmod n $$$

Lean4

theorem val_mul {n : ℕ} (a b : ZMod n) : (a * b).val = a.val * b.val % n :=
  by
  cases n
  · rw [Nat.mod_zero]
    apply Int.natAbs_mul
  · apply Fin.val_mul

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