mod_add_div'

Mathlib.Algebra.EuclideanDomain.Defs

URI: https://scilib.ai/kg/mathlib#EuclideanDomain.mod_add_div'

English

For any R in a Euclidean domain, a / b · b + a % b = a.

Русский

Для любого a,b в евклидовом кольце a / b · b + a % b = a.

LaTeX

$$$$ (a / b) \\cdot b + a \\% b = a. $$$$

Lean4

theorem mod_add_div' (m k : R) : m % k + m / k * k = m :=
  by
  rw [mul_comm]
  exact mod_add_div _ _

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

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

Разделы

Аффилиация

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