isUnit_Δ

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.isUnit_Δ

English

For an elliptic Weierstrass curve W, Δ is a unit in R: IsUnit W.Δ.

Русский

Для эллиптической кривой Вейерштрасса W дискриминант Δ является единицей в R: IsUnit W.Δ.

LaTeX

$$$ \mathrm{IsUnit}(W.\Delta) $$$

Lean4

theorem isUnit_Δ : IsUnit W.Δ :=
  IsElliptic.isUnit

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

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

Разделы

Аффилиация

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