map_Ψ₃

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.map_Ψ₃

English

(W.map f).Ψ₃ = W.Ψ₃.map f; Ψ3 commutes with base change.

Русский

(W.map f).Ψ₃ = W.Ψ₃.map f; Ψ3 совместим с переходом базы.

LaTeX

$$$ (W.map f).\\Psi_3 = W.\\Psi_3.map f $$$

Lean4

@[simp]
theorem map_Ψ₃ : (W.map f).Ψ₃ = W.Ψ₃.map f := by simp [Ψ₃]

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

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

Разделы

Аффилиация

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