map_b₆

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.map_b₆

English

Similarly, (W.map f).b₆ = f(W.b₆).

Русский

Аналогично, (W.map f).b₆ = f(W.b₆).

LaTeX

$$$ (W.map f).b_6 = f(W.b_6) $$$

Lean4

@[simp]
theorem map_b₆ : (W.map f).b₆ = f W.b₆ := by
  simp only [b₆, map_a₃, map_a₆]
  map_simp

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

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

Разделы

Аффилиация

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