div_div_cancel

Mathlib.Data.ENNReal.Inv

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

← MathLib Explorer

English

If a ≠ 0 and a ≠ ∞, then a / (a / b) = b.

Русский

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

LaTeX

$$ (a ≠ 0) ∧ (a ≠ ∞) ⇒ \dfrac{a}{(a/b)} = b $$

Lean4

/-- See `ENNReal.div_div_cancel'` for a stronger version. -/
protected theorem div_div_cancel {a b : ℝ≥0∞} (h₀ : a ≠ 0) (h₁ : a ≠ ∞) : a / (a / b) = b :=
  ENNReal.div_div_cancel' (by simp [h₀]) (by simp [h₁])

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

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

Разделы

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

Аффилиация

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