Δ_integral_of_isIntegral — Mathlib

English

For W integral over R, there exists r in R such that algebraMap R K r = W.Δ.

Русский

Для W целочисленной над R существует r ∈ R, такой что algebraMap R K r = W.Δ.

LaTeX

$$$\\exists r \\; (algebraMap\\ R\\ K)(r) = W.Δ$$$

Lean4

theorem Δ_integral_of_isIntegral (W : WeierstrassCurve K) [IsIntegral R W] : ∃ r : R, algebraMap R K r = W.Δ :=
  by
  obtain ⟨W_int, hW_int⟩ : ∃ W_int : WeierstrassCurve R, W = W_int.baseChange K := IsIntegral.integral
  use W_int.Δ
  rw [hW_int, map_Δ]

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