toCharTwoJNeZeroNF_spec — Mathlib

English

In char-two-zero-normal-form, c6 = 0.

Русский

В нормальной форме charTwoJEqZeroNF, c6 = 0.

LaTeX

$$$W.c_6 = 0$$$

Lean4

theorem toCharTwoJNeZeroNF_spec (ha₁ : W.a₁ ≠ 0) : (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoJNeZeroNF :=
  by
  constructor
  · simp [toCharTwoJNeZeroNF, ha₁, variableChange_a₁]
  · simp [field, toCharTwoJNeZeroNF, variableChange_a₃, -mul_eq_zero]
    linear_combination (W.a₃ * W.a₁ ^ 3 + W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) * CharP.cast_eq_zero F 2
  · simp [field, toCharTwoJNeZeroNF, variableChange_a₄, -mul_eq_zero]
    linear_combination (W.a₃ ^ 2 + W.a₁ * W.a₃ * W.a₂) * CharP.cast_eq_zero F 2

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