mul_left' — Mathlib

English

If a ≡ b (mod n), then c a ≡ c b (mod c n).

Русский

Если a ≡ b (mod n), то c a ≡ c b (mod c n).

LaTeX

$$$a \equiv b \pmod n \Rightarrow c a \equiv c b \pmod{c n}$$$

Lean4

protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] :=
  by
  obtain hc | rfl | hc := lt_trichotomy c 0
  · rw [← neg_modEq_neg, ← modEq_neg, ← Int.neg_mul, ← Int.neg_mul, ← Int.neg_mul]
    simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]
  · simp only [Int.zero_mul, ModEq.rfl]
  · simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq]

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