instMulDivCancelClass

Mathlib.Algebra.Ring.Int.Defs

URI: https://scilib.ai/kg/mathlib#Int.instMulDivCancelClass

English

For integers m,n, the division-cancellation law holds: if a ≠ 0 then ab = ac implies b = c.

Русский

Для целых чисел m,n выполняется закон отмены деления: если a ≠ 0, то ab = ac вызывает b = c.

LaTeX

$$$\forall a,b,c \in \mathbb{Z},\ a \neq 0 \Rightarrow ab = ac \Rightarrow b = c$$$

Lean4

instance instMulDivCancelClass : MulDivCancelClass ℤ where mul_div_cancel _ _ := mul_ediv_cancel _

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

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

Разделы

Аффилиация

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