toCharNeTwoNF_spec — Mathlib

English

The operation of taking CharNeTwoNF preserves the CharNeTwoNF property of the curve after the coordinate change.

Русский

Преобразование к нормальной форме сохраняет свойство ≠ 2 для кривой после изменения координат.

LaTeX

$$$$ (W.toCharNeTwoNF \; • \; W).IsCharNeTwoNF $$$$

Lean4

instance toCharNeTwoNF_spec : (W.toCharNeTwoNF • W).IsCharNeTwoNF := by
  constructor <;> simp [variableChange_a₁, variableChange_a₃]

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