coe_div

Mathlib.Data.ENNReal.Inv

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

English

If r ≠ 0, then coercion commutes with division: ↑(p / r) = p / r.

Русский

Если r ≠ 0, приводление сохраняет деление: ↑(p / r) = p / r.

LaTeX

$$↑(p / r) = p / r$$

Lean4

@[simp, norm_cast]
theorem coe_div (hr : r ≠ 0) : (↑(p / r) : ℝ≥0∞) = p / r := by rw [div_eq_mul_inv, div_eq_mul_inv, coe_mul, coe_inv hr]

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

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

Разделы

Аффилиация

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