coe_div — Mathlib

English

For all real numbers a,b, the division in Real corresponds to division in EReal via the embedding: (a/b)_{Real} = (a:EReal)/(b:EReal).

Русский

Для любых вещественных a,b деление в Real соответствует делению в EReal через вложение: (a/b)_{Real} = (a:EReal)/(b:EReal).

LaTeX

$$$ (a/b:\!\mathbb{R}) = (a:\!\mathrm{EReal}) / (b:\!\mathrm{EReal}) $$$

Lean4

theorem coe_div (a b : ℝ) : (a / b : ℝ) = (a : EReal) / (b : EReal) :=
  rfl

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