inv_variableChange_Δ'

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

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

English

The inverse of the transformed Δ' scales by u^{12}: (Δ')^{-1} transforms as Δ'^{-1} = u^{12} Δ^{-1}.

Русский

Обратное к преобразованному Δ' масштабируется как Δ'^{-1} = u^{12} Δ^{-1}.

LaTeX

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

Lean4

theorem inv_variableChange_Δ' : (C • W).Δ'⁻¹ = C.u ^ 12 * W.Δ'⁻¹ := by rw [variableChange_Δ', mul_inv, inv_pow, inv_inv]

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

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

Разделы

Аффилиация

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