XIdeal

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Affine.CoordinateRing.XIdeal

Lean4

/-- The ideal `⟨X - x⟩` of `R[W]` for some `x` in `R`. -/
noncomputable def XIdeal (x : R) : Ideal W'.CoordinateRing :=
  .span {XClass W' x}

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

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

Разделы

Аффилиация

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