instIsScalarTowerPolynomial

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

English

Similarly to exists_smul_basis_eq, there exist p,q with p•1 + q•mk W' Y = x.

Русский

Аналогично смыслу exists_smul_basis_eq, существуют p,q такие, что p•1 + q•mk W' Y = x.

LaTeX

$$$\exists p\,\exists q\, (p \cdot (1 : W'.CoordinateRing) + q \cdot mk W' Y) = x$$$

Lean4

instance : IsScalarTower R R[X] W'.CoordinateRing :=
  Quotient.isScalarTower R R[X] _

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

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

Разделы

Аффилиация

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