map_ψ₂

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.map_ψ₂

English

(W.map f).ψ₂ = W.ψ₂.map (mapRingHom f); i.e., ψ₂ commutes with base change.

Русский

(W.map f).ψ₂ = W.ψ₂.map (mapRingHom f); то же свойство совместимости с переходом базы.

LaTeX

$$$ (W.map f).\\psi_2 = W.\\psi_2.map(\\mathrm{mapRingHom}\, f) $$$

Lean4

@[simp]
theorem map_ψ₂ : (W.map f).ψ₂ = W.ψ₂.map (mapRingHom f) := by simp_rw [ψ₂, Affine.map_polynomialY]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru