toCharTwoJEqZeroNF_spec — Mathlib

English

Under char-two-zero-normal-form in characteristic two, b8 = a4^2.

Русский

При характеристике 2 и нормальной форме charTwoJEqZeroNF, b8 = a4^2.

LaTeX

$$$W.b_8 = W.a_4^{2}$$$

Lean4

theorem toCharTwoJEqZeroNF_spec (ha₁ : W.a₁ = 0) : (W.toCharTwoJEqZeroNF • W).IsCharTwoJEqZeroNF :=
  by
  constructor
  · simp [toCharTwoJEqZeroNF, ha₁, variableChange_a₁]
  · simp_rw [toCharTwoJEqZeroNF, variableChange_a₂, inv_one, Units.val_one]
    linear_combination 2 * W.a₂ * CharP.cast_eq_zero R 2

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