coe_inv_map_Δ'

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

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

English

The inverse of Δ' after base-change corresponds to the image under f of the original inverse Δ'^{-1}.

Русский

Обратное к Δ' после базисного переноса соответствует образу исходного Δ'^{-1} под f.

LaTeX

$$(W.map f).Δ'^{-1} = f( W.Δ'^{-1} )$$

Lean4

theorem coe_inv_map_Δ' : (W.map f).Δ'⁻¹ = f ↑W.Δ'⁻¹ := by simp

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

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

Разделы

Аффилиация

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