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⟩