IsCharTwoNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.IsCharTwoNF

Lean4

/-- A `WeierstrassCurve` is in normal form of characteristic = 2, if it is
`Y² + XY = X³ + a₂X² + a₆` (`WeierstrassCurve.IsCharTwoJNeZeroNF`) or
`Y² + a₃Y = X³ + a₄X + a₆` (`WeierstrassCurve.IsCharTwoJEqZeroNF`). -/
class inductive IsCharTwoNF : Prop
  | of_j_ne_zero [W.IsCharTwoJNeZeroNF] : IsCharTwoNF
  | of_j_eq_zero [W.IsCharTwoJEqZeroNF] : IsCharTwoNF

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

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

Разделы

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

Аффилиация

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