natDegree_norm_ne_one — Mathlib

English

The natural degree of the norm of any coordinate ring element is not equal to 1.

Русский

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

LaTeX

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

Lean4

theorem natDegree_norm_ne_one [IsDomain R] (x : W'.CoordinateRing) : (Algebra.norm R[X] x).natDegree ≠ 1 :=
  degree_norm_ne_one x ∘ (degree_eq_iff_natDegree_eq_of_pos zero_lt_one).mpr

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