smul — Mathlib

English

If h is an elliptic sequence, then for any scalar x ∈ R, the scaled sequence x•W is also an elliptic sequence.

Русский

Если h — эллиптическая последовательность, то для любого скаляра x ∈ R последовательность x•W тоже эллиптическая.

LaTeX

$$$ IsEllSequence(W) \Rightarrow IsEllSequence(x\cdot W) $$$

Lean4

theorem smul (h : IsEllSequence W) (x : R) : IsEllSequence (x • W) := fun m n r => by
  linear_combination (norm := (simp_rw [Pi.smul_apply, smul_eq_mul]; ring1)) x ^ 4 * h m n r

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