instMul

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.VariableChange.instMul

Lean4

instance : Mul (VariableChange R) where
  mul C
    C' :=
    { u := C.u * C'.u
      r := C.r * C'.u ^ 2 + C'.r
      s := C'.u * C.s + C'.s
      t := C.t * C'.u ^ 3 + C.r * C'.s * C'.u ^ 2 + C'.t }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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