YClass

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

Lean4

/-- The class of the element `Y - y(X)` in `R[W]` for some `y(X)` in `R[X]`. -/
noncomputable def YClass (y : R[X]) : W'.CoordinateRing :=
  mk W' <| Y - C y

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

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

Разделы

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

Аффилиация

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