div_eq_inv_mul

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.div_eq_inv_mul

English

For any a,b ∈ EReal, a / b = b^{-1} · a (equivalently a / b = a · b^{-1} by commutativity).

Русский

Для любых a,b ∈ EReal имеем: a / b = b^{-1} · a (или a · b^{-1} по коммутативности).

LaTeX

$$$ a / b = b^{-1} \cdot a $$$

Lean4

protected theorem div_eq_inv_mul (a b : EReal) : a / b = b⁻¹ * a :=
  EReal.mul_comm a b⁻¹

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

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

Разделы

Аффилиация

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