coe_ofScientific — Mathlib

English

The coercion from OfScientific to the ambient field K in the nonnegative subtype is the identity on the underlying value.

Русский

Приведение OfScientific к окружному полю K в неотрицательном подтипе совпадает по значению с исходным числом.

LaTeX

$$$ \operatorname{val} \left( \mathrm{OfScientific.ofScientific}(m,s,e) : \{ x : K \mid 0 \le x \} \right) = \mathrm{OfScientific.ofScientific}(m,s,e). $$$

Lean4

theorem coe_ofScientific {K} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (m : ℕ) (s : Bool) (e : ℕ) :
    (ofScientific m s e : { x : K // 0 ≤ x }).val = ofScientific m s e :=
  rfl

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