trunc — Mathlib

English

For a ∈ R and f ∈ R⟦X⟧, rescaling by the constant function a equals the standard rescale by a, i.e., MvPowerSeries.rescale(constant a) f = rescale a f.

Русский

Для a ∈ R и f ∈ R⟦X⟧ при масштабе по константе a получается то же самое, что и обычное масштабирование: MvPowerSeries.rescale(constant a) f = rescale a f.

LaTeX

$$$\\text{MvPowerSeries.rescale}(\\text{Function.const }_{}\\, a)\\, f = \\text{rescale}\\ a\\ f$$$

Lean4

/-- The `n`th truncation of a formal power series to a polynomial -/
def trunc (n : ℕ) (φ : R⟦X⟧) : R[X] :=
  ∑ m ∈ Ico 0 n, Polynomial.monomial m (coeff m φ)

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