Δ' — Mathlib

English

Let Δ' denote the unit of R corresponding to Δ(W) via the elliptic-is-elliptic structure: Δ' = (W. isUnit_Δ).unit.

Русский

Обозначим Δ' единицу кольца R, соответствующую Δ(W) через структуру эллиптической кривой: Δ' = (W.isUnit_Δ).unit.

LaTeX

$$$ \Delta' = W.\text{isUnit_Δ}.\text{unit} $$$

Lean4

/-- The discriminant `Δ'` of an elliptic curve over `R`, which is given as a unit in `R`.
Note that to prove two equal elliptic curves have the same `Δ'`, you need to use `simp_rw`,
as `rw` cannot transfer instance `WeierstrassCurve.IsElliptic` automatically. -/
noncomputable def Δ' : Rˣ :=
  W.isUnit_Δ.unit

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