of_mul_right — Mathlib

English

Cancel right multiplication in the modulus: from a ≡ b (mod n·m) deduce a ≡ b (mod n).

Русский

Отмена правого умножения в модуле: из a ≡ b (mod n·m) следует a ≡ b (mod n).

LaTeX

$$$ (m : Nat) \Rightarrow a \equiv b [MOD n m] \Rightarrow a \equiv b [MOD n] $$$

Lean4

/-- Cancel right multiplication in the modulus.

For cancelling right multiplication on both sides of the `≡`, see `nat.modeq.mul_right_cancel'`. -/
theorem of_mul_right (m : ℕ) : a ≡ b [MOD n * m] → a ≡ b [MOD n] :=
  mul_comm m n ▸ of_mul_left _

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