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_8 = f(W.b_8) $$$

Lean4

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

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

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

Разделы

Аффилиация

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