instCancelCommMonoidWithZero

Mathlib.Algebra.Ring.Int.Defs

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

English

In the integers, if a ≠ 0 and ab = ac, then b = c.

Русский

В целых числах, если 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 instCancelCommMonoidWithZero : CancelCommMonoidWithZero ℤ where
  mul_left_cancel_of_ne_zero ha _ _ := (mul_eq_mul_left_iff ha).1

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

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

Разделы

Аффилиация

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