basis_zero

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

English

The basis at index 1 equals mk W' Y.

Русский

База на индексe 1 равна mk W' Y.

LaTeX

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

Lean4

@[simp]
theorem basis_zero : CoordinateRing.basis W' 0 = 1 := by simpa only [basis_apply] using pow_zero _

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

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

Разделы

Аффилиация

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