variableChange_Δ'

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

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

← MathLib Explorer

English

The transformed discriminant Δ' scales by u^{-12} when applying the change C.

Русский

После применения преобразования C дискриминант Δ' масштабируется как u^{-12}.

LaTeX

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

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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