map — Mathlib

English

If f: R →+* A is a ring homomorphism, then the Weierstrass curve over A given by applying f to the coefficients of W is W.map f.

Русский

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

LaTeX

$$$ (W.map f) = \langle f(W.a_1), f(W.a_2), f(W.a_3), f(W.a_4), f(W.a_6) \rangle $$$

Lean4

/-- The Weierstrass curve mapped over a ring homomorphism `f : R →+* A`. -/
@[simps]
def map : WeierstrassCurve A :=
  ⟨f W.a₁, f W.a₂, f W.a₃, f W.a₄, f W.a₆⟩

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