dvd_mod_iff — Mathlib

English

If c divides b, then c divides a % b if and only if c divides a: c ∣ b ⇒ (c ∣ a % b) ⇔ (c ∣ a).

Русский

Если c делит b, то c делит a % b тогда и только тогда, когда c делит a: c | b ⇒ (c | a % b) ⇔ (c | a).

LaTeX

$$$ c \mid b \;\Rightarrow\; (c \mid a \% b) \iff (c \mid a) $$$

Lean4

theorem dvd_mod_iff {a b c : R} (h : c ∣ b) : c ∣ a % b ↔ c ∣ a := by rw [← dvd_add_right (h.mul_right _), div_add_mod]

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