c₄_of_char_two

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

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

English

If the base ring has characteristic two, then c4 equals a1^4.

Русский

При характеристике 2 c4 = a1^4.

LaTeX

$$$$ W.c_4 = W.a_1^4 $$$$

Lean4

theorem c₄_of_char_two : W.c₄ = W.a₁ ^ 4 := by
  rw [c₄, b₂_of_char_two]
  linear_combination -12 * W.b₄ * CharP.cast_eq_zero R 2

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

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

Разделы

Аффилиация

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