single_zero_ofScientific — Mathlib

English

The evaluation of a scientific notation single term at a zero index reduces to the scientific constant.

Русский

Значение единичного терма в научной нотации при нулевой степени сводится к константе научного выражения.

LaTeX

$$ single (0 : Γ) (OfScientific.ofScientific m e s : R) = OfScientific.ofScientific m e s $$

Lean4

theorem single_zero_ofScientific (m e s) :
    single (0 : Γ) (OfScientific.ofScientific m e s : R) = OfScientific.ofScientific m e s := by
  simpa using single_zero_ratCast (Γ := Γ) (R := R) (OfScientific.ofScientific m e s)

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