coe_map_Δ'

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

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

English

Under a ring hom f, the discriminant Δ' of the base-changed curve equals the image of the original discriminant under f:

Русский

При отображении колец f дискриминант Δ' кривой после базисного переноса равен образу исходного Δ' под f.

LaTeX

$$(W.map f).Δ' = f(W.Δ')$$

Lean4

theorem coe_map_Δ' : (W.map f).Δ' = f W.Δ' := by rw [coe_Δ', map_Δ, coe_Δ']

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

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

Разделы

Аффилиация

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