degree_norm_ne_one — Mathlib

English

For any x in the coordinate ring of W, the degree of the norm is never equal to 1.

Русский

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

LaTeX

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

Lean4

theorem degree_norm_ne_one [IsDomain R] (x : W'.CoordinateRing) : (Algebra.norm R[X] x).degree ≠ 1 :=
  by
  rcases exists_smul_basis_eq x with ⟨p, q, rfl⟩
  rw [degree_norm_smul_basis]
  rcases p.degree with (_ | _ | _ | _) <;> cases q.degree
  any_goals rintro (_ | _)
  exact (lt_max_of_lt_right <| (cmp_eq_lt_iff ..).mp rfl).ne'

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