one_lt_absNorm — Mathlib

English

The norm of a height-one maximal ideal is strictly greater than 1.

Русский

Норма максимального идеала высоты единицы больше единицы.

LaTeX

$$$1 < \operatorname{absNorm}(v.asIdeal)$$$

Lean4

/-- The norm of a maximal ideal is `> 1` -/
theorem one_lt_absNorm : 1 < absNorm v.asIdeal := by
  by_contra! h
  apply IsPrime.ne_top v.isPrime
  rw [← absNorm_eq_one_iff]
  have : 0 < absNorm v.asIdeal := by
    rw [Nat.pos_iff_ne_zero, absNorm_ne_zero_iff]
    exact v.asIdeal.finiteQuotientOfFreeOfNeBot v.ne_bot
  cutsat

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