ofScientific_eq_ofScientific — Mathlib

English

The scalar-to-Rat numeric notation is simp-normal form: Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) equals OfScientific.ofScientific m s e.

Русский

Симп-нормальная форма записи Scientific: Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) равняется OfScientific.ofScientific m s e.

LaTeX

$$$\text{Rat.ofScientific} (\text{OfNat.ofNat } m)\; s\; (\text{OfNat.ofNat } e) = \text{OfScientific.ofScientific } m\; s\; e$$$

Lean4

/-- `OfScientific.ofScientific` is the simp-normal form. -/
@[simp]
theorem ofScientific_eq_ofScientific (m : ℕ) (s : Bool) (e : ℕ) :
    Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e :=
  rfl

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