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_4 = f(W.b_4) $$$

Lean4

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

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

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

Разделы

Аффилиация

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