mul_inv_cancel_left

Mathlib.Data.ENNReal.Inv

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

← MathLib Explorer

English

If a ≠ 0 and a ≠ ∞ then a · (a⁻¹ · b) = b.

Русский

Если a ≠ 0 и a ≠ ∞, то a · (a⁻¹ · b) = b.

LaTeX

$$$a \neq 0 \land a \neq \infty \Rightarrow a \cdot (a^{-1} \cdot b) = b$$$

Lean4

/-- See `ENNReal.mul_inv_cancel_left'` for a stronger version. -/
protected theorem mul_inv_cancel_left (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * (a⁻¹ * b) = b :=
  ENNReal.mul_inv_cancel_left' (by simp [ha₀]) (by simp [ha])

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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