instIsLeftCancelMulZero

Mathlib.Algebra.GroupWithZero.Nat

URI: https://scilib.ai/kg/mathlib#Nat.instIsLeftCancelMulZero

English

IsLeftCancelMulZero ℕ: if a ≠ 0 and ab = ac then b = c.

Русский

Левостороннее отменение умножения на ноль в ℕ: если a ≠ 0 и ab = ac, тогда b = c.

LaTeX

$$$a \\neq 0 \\Rightarrow (ab = ac \\Rightarrow b = c) \\\\text{ for } a,b,c \\in \\mathbb{N}$$$

Lean4

instance instIsLeftCancelMulZero : IsLeftCancelMulZero ℕ where
  mul_left_cancel_of_ne_zero h _ _ := Nat.eq_of_mul_eq_mul_left (Nat.pos_of_ne_zero h)

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

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

Разделы

Аффилиация

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