map_Δ

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

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

English

The discriminant also commutes with map: (W.map f).Δ = f(W.Δ).

Русский

Дискриминант также сохраняется под отображением: (W.map f).Δ = f(W.Δ).

LaTeX

$$$ (W.map f).\Delta = f(W.\Delta) $$$

Lean4

@[simp]
theorem map_Δ : (W.map f).Δ = f W.Δ :=
  by
  simp only [Δ, map_b₂, map_b₄, map_b₆, map_b₈]
  map_simp

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

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

Разделы

Аффилиация

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