IsCharThreeNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

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

Lean4

/-- A `WeierstrassCurve` is in normal form of characteristic = 3, if it is
`Y² = X³ + a₂X² + a₆` (`WeierstrassCurve.IsCharThreeJNeZeroNF`) or
`Y² = X³ + a₄X + a₆` (`WeierstrassCurve.IsShortNF`). -/
class inductive IsCharThreeNF : Prop
  | of_j_ne_zero [W.IsCharThreeJNeZeroNF] : IsCharThreeNF
  | of_j_eq_zero [W.IsShortNF] : IsCharThreeNF

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

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

Разделы

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

Аффилиация

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