instInv

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

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

Lean4

instance : Inv (VariableChange R) where
  inv
    C :=
    { u := C.u⁻¹
      r := -C.r * C.u⁻¹ ^ 2
      s := -C.s * C.u⁻¹
      t := (C.r * C.s - C.t) * C.u⁻¹ ^ 3 }

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

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

Разделы

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

Аффилиация

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