instMulDivCancelClass

Mathlib.Algebra.GroupWithZero.Nat

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

English

MulDivCancelClass ℕ: mul_div_cancel a b b_H assigns a * b / b = a when b ≠ 0.

Русский

MulDivCancelClass ℕ: mul_div_cancel a b b_H даёт a * b / b = a при b ≠ 0.

LaTeX

$$$a \\cdot b / b = a \\quad\\text{for } b \\neq 0$$$

Lean4

instance instMulDivCancelClass : MulDivCancelClass ℕ where
  mul_div_cancel _ _b hb := Nat.mul_div_cancel _ (Nat.pos_iff_ne_zero.2 hb)

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

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

Разделы

Аффилиация

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