dblZ_smul

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Projective.dblZ_smul

English

For P and u, W'.dblZ(u•P) = u^4 W'.dblZ P.

Русский

Для P и скаляра u выполняется равенство W'.dblZ(u•P) = u^4 W'.dblZ P.

LaTeX

$$W'.dblZ (u \cdot P) = u^4 · W'.dblZ P$$

Lean4

theorem dblZ_smul (P : Fin 3 → R) (u : R) : W'.dblZ (u • P) = u ^ 4 * W'.dblZ P :=
  by
  simp only [dblZ, negY_smul, smul_fin3_ext]
  ring1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru