some_ne_zero

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

English

For any x in the coordinate ring, the natural degree of the norm is not equal to 1 (general form).

Русский

Для любого x в координатном кольце естественная степень нормы не равна 1.

LaTeX

$$$\\operatorname{natDegree}(\\operatorname{norm}_{R[X]}(x)) \\neq 1$$$

Lean4

theorem some_ne_zero {x y : R} (h : W'.Nonsingular x y) : Point.some h ≠ 0 := by rintro (_ | _)

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

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

Разделы

Аффилиация

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