valuation_Δ_aux — Mathlib

English

There exists a variable change C such that W transformed by C is integral over R.

Русский

Существует переменная смены C так, что W, преобразованная умножением C, целична по отношению к R.

LaTeX

$$$\\exists C : \\text{VariableChange} K,\\; \\text{IsIntegral } R (C \\cdot W)$$$

Lean4

/-- The valuation of the discriminant of a Weierstrass curve `W`,
which is at most 1 if `W` is integral. Zero otherwise. -/
noncomputable def valuation_Δ_aux (W : WeierstrassCurve K) : { v : ℤᵐ⁰ // v ≤ 1 } :=
  if h : IsIntegral R W then
    ⟨valuation K (maximalIdeal R) W.Δ,
      by
      choose r hr using Δ_integral_of_isIntegral R W
      rw [← hr]
      exact valuation_le_one (maximalIdeal R) r⟩
  else ⟨⊥, bot_le⟩

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