coe_variableChange_Δ'

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.coe_variableChange_Δ'

English

The coerced Δ' under a change C scales as Δ' = (u^{-12}) Δ'.

Русский

Коэрцированный Δ' при изменении C масштабируется как Δ' = u^{-12} Δ'.

LaTeX

$$$((C \\cdot W).\\Delta') = C.u^{-12} W.\\Delta'. $$$

Lean4

theorem coe_variableChange_Δ' : ((C • W).Δ' : R) = C.u⁻¹ ^ 12 * W.Δ' := by simp_rw [coe_Δ', variableChange_Δ]

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

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

Разделы

Аффилиация

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