coe_ofScientific — Mathlib

English

For m, s, e, the real-valued coercion of OfScientific.ofScientific(m,s,e) in NNReal equals OfScientific.ofScientific(m,s,e) in Real.

Русский

Для m, s, e преобразование in Real от OfScientific.ofScientific(m,s,e) в NNReal равно OfScientific.ofScientific(m,s,e) в Real.

LaTeX

$$$↑(OfScientific.ofScientific(m,s,e) : \mathbb{R}_{\ge 0}) = (OfScientific.ofScientific(m,s,e) : \mathbb{R})$$$

Lean4

@[simp, norm_cast]
protected theorem coe_ofScientific (m : ℕ) (s : Bool) (e : ℕ) :
    ↑(OfScientific.ofScientific m s e : ℝ≥0) = (OfScientific.ofScientific m s e : ℝ) :=
  rfl

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