smul — Mathlib

English

If h is an Elliptic Divisibility Sequence, then scaling W by x preserves the Elliptic Divisibility structure: (x•W) is again an Elliptic Divisibility Sequence.

Русский

Если W — Эллиптическая Последовательность Делимости, то умножение на скаляр сохраняет структуру: x•W снова является ЭДС.

LaTeX

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

Lean4

theorem smul (h : IsDivSequence W) (x : R) : IsDivSequence (x • W) := fun m n r => mul_dvd_mul_left x <| h m n r

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