negY_smul

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

English

Scaling a projective point P by a scalar u scales its negY by the same scalar in the appropriate product.

Русский

Умножение точки P на скаляр u масштабирует значение negY на тот же скаляр.

LaTeX

$$$ W'.negY (u \\cdot P) = u \\cdot W'.negY P $$$

Lean4

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

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

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

Разделы

Аффилиация

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