toClass_some

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Affine.Point.toClass_some

English

The toClass_some equality expresses that the class map respects the 'some' construction for nonsingular points.

Русский

Неравенство toClass_some выражает сохранение отображения по точкам через конструкцию some.

LaTeX

$$toClass_some(h) = XYIdeal'(h)$$

Lean4

theorem toClass_some {x y : F} (h : W.Nonsingular x y) : toClass (some h) = ClassGroup.mk (CoordinateRing.XYIdeal' h) :=
  rfl

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

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

Разделы

Аффилиация

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