self_mul_add

Mathlib.Data.Nat.ModEq

URI: https://scilib.ai/kg/mathlib#Nat.ModEq.self_mul_add

English

For all m, a, b, we have m·a + b ≡ b (mod m).

Русский

Для любых m, a, b верно m·a + b ≡ b (mod m).

LaTeX

$$$m a + b \\equiv b \\pmod{m}$$$

Lean4

theorem self_mul_add : ModEq m (m * a + b) b := by simp [Nat.ModEq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru