div_self

Mathlib.Data.ENNReal.Inv

URI: https://scilib.ai/kg/mathlib#ENNReal.div_self

English

If b = c/a with a ≠ 0, a ≠ ∞, then a b = c.

Русский

Если b = c/a и a ≠ 0, a ≠ ∞, тогда a b = c.

LaTeX

$$$b = \\dfrac{c}{a} \\iff a b = c \\quad (a\\neq0, a\\neq\\infty)$$$

Lean4

protected theorem div_self (h0 : a ≠ 0) (hI : a ≠ ∞) : a / a = 1 :=
  ENNReal.mul_inv_cancel h0 hI

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

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

Разделы

Аффилиация

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