toShortNF_spec — Mathlib

English

There is an explicit short-normal-form change relative to W, and the transformed curve (W.toShortNF • W) is in short NF.

Русский

Существует явное преобразование к краткой нормальной форме относительно W, и преобразованная кривая (W.toShortNF • W) находится в краткой НФ.

LaTeX

$$$ (W\text{ toShortNF }\cdot W) \text{ is in short NF} $$$

Lean4

instance toShortNF_spec : (W.toShortNF • W).IsShortNF :=
  by
  rw [toShortNF, mul_smul]
  constructor <;> simp [variableChange_a₁, variableChange_a₂, variableChange_a₃]

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