XClass

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

← MathLib Explorer

English

For nontrivial rings, the element XClass W' x is nonzero for any x ∈ R.

Русский

Для ненулевых колец элемент XClass W' x ненулевой для любого x ∈ R.

LaTeX

$$XClass W' x ≠ 0$$

Lean4

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

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

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

Разделы

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

Аффилиация

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