integralModel_Δ_eq — Mathlib

English

The Δ of the integral model matches the original Δ: algebraMap R K (integralModel R W).Δ = W.Δ.

Русский

Δ интегральной модели совпадает с исходным Δ: algebraMap R K (integralModel R W).Δ = W.Δ.

LaTeX

$$$\\operatorname{algebraMap}\\ R\\ K\\left((\\operatorname{integralModel}\\ R\\ W).\\Delta\\right) = W.\\Delta$$$

Lean4

theorem integralModel_Δ_eq (W : WeierstrassCurve K) [hW : IsIntegral R W] :
    algebraMap R K (integralModel R W).Δ = W.Δ :=
  by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [integralModel]

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