coe_div — Mathlib

English

Coercion commutes with division: the real value of the division in NNReal equals the division of real values.

Русский

Коэрцирование сохраняет деление: действительное значение дроби в NNReal равно делению действительных значений.

LaTeX

$$$ ((r_1 / r_2 : \mathbb{R}_{\ge 0}) : \mathbb{R}) = (r_1 : \mathbb{R}) / r_2 $$$

Lean4

@[simp, norm_cast]
protected theorem coe_div (r₁ r₂ : ℝ≥0) : ((r₁ / r₂ : ℝ≥0) : ℝ) = (r₁ : ℝ) / r₂ :=
  rfl

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