zero_div

Mathlib.Algebra.EuclideanDomain.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanDomain.zero_div

← MathLib Explorer

English

In a Euclidean domain, the remainder equals a minus b times the quotient: a % b = a − b · (a / b).

Русский

В евклидовом кольце остаток равен a − b · (a / b).

LaTeX

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

Lean4

@[simp]
theorem zero_div {a : R} : 0 / a = 0 :=
  by_cases (fun a0 : a = 0 => a0.symm ▸ div_zero 0) fun a0 => by simpa only [zero_mul] using mul_div_cancel_right₀ 0 a0

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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