map_c₆

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

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

English

Similarly, (W.map f).c6 = f(W.c6).

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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