basis_one

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

English

The basis coefficients align with evaluation at X in the polynomial ring, via mk W' X.

Русский

Коэффициенты базы согласуются с вычислением в X в кольце многочленов через mk W' X.

LaTeX

$$$ CoordinateRing.basis W' 1 = mk W' Y$$$

Lean4

@[simp]
theorem basis_one : CoordinateRing.basis W' 1 = mk W' Y := by simpa only [basis_apply] using pow_one _

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

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

Разделы

Аффилиация

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