exists_variableChange_isShortNF — Mathlib

English

There exists a variable change C such that the transformed curve C • W is in short NF.

Русский

Существует преобразование переменных C так, что преобразованная кривая C • W находится в краткой нормальной форме.

LaTeX

$$$\exists C:\mathrm{VariableChange}(R),\ (C\cdot W).IsShortNF$$$

Lean4

theorem exists_variableChange_isShortNF : ∃ C : VariableChange R, (C • W).IsShortNF :=
  ⟨_, W.toShortNF_spec⟩

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