map_Δ' — Mathlib

English

Under a ring hom f, the discriminant Δ' of the base-changed curve is the image under units.map f of the original Δ':

Русский

При отображении колец f дискриминант Δ' кривой после базисного переноса равен образу Δ' под отображением единиц.

LaTeX

$$(W.map f).Δ' = Units.map f W.Δ'$$

Lean4

@[simp]
theorem map_Δ' : (W.map f).Δ' = Units.map f W.Δ' := by
  ext
  exact W.coe_map_Δ' f

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