map_c₄

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

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

English

In char 3, the c4 coefficient maps under f: (W.map f).c4 = f(W.c4).

Русский

В характеристике 3 коэффициент c4 отображается по f: (W.map f).c4 = f(W.c4).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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