exists_variableChange_isCharThreeNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

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

English

There exists a variable change C such that (C • W).IsCharThreeNF.

Русский

Существует изменение переменных C такое, что (C • W).IsCharThreeNF.

LaTeX

$$$\exists C : \mathrm{VariableChange}(F),\ (C \cdot W).IsCharThreeNF$$$

Lean4

theorem exists_variableChange_isCharThreeNF : ∃ C : VariableChange F, (C • W).IsCharThreeNF :=
  ⟨_, W.toCharThreeNF_spec⟩

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

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

Разделы

Аффилиация

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