instIsEllipticMap — Mathlib

English

If W is an elliptic Weierstrass curve over R and f: R → A is a ring hom, then the base-changed curve W.map f is elliptic over A.

Русский

Если W — эллиптическая кривая Вейерштрасса над R и f: R → A — гомоморфизм колец, то база-перемещение W.map f дает эллиптическую кривую над A.

LaTeX

$$(W.map f).IsElliptic$$

Lean4

instance : (W.map f).IsElliptic := by simp only [isElliptic_iff, map_Δ, W.isUnit_Δ.map]

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