ofJ_ne_0_ne_1728

Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.ofJ_ne_0_ne_1728

English

If 2 ≠ 0 in F, then the model with j=1728 is equal to ofJ1728 F, provided 3 ≠ 0 as needed.

Русский

Если 2 ≠ 0 в F, то модель with j=1728 совпадает с ofJ1728 F при необходимых условиях на 3.

LaTeX

$$$$ ofJ 1728 = ofJ1728 F $$$$

Lean4

theorem ofJ_ne_0_ne_1728 (h0 : j ≠ 0) (h1728 : j ≠ 1728) : ofJ j = ofJNe0Or1728 j := by
  rw [ofJ, if_neg h0, if_neg h1728]

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

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

Разделы

Аффилиация

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