toCharThreeNF_spec_of_b₂_eq_zero

English

If hb₂: W.b₂ = 0, then the CharThreeNF built from CharThreeNF yields a ShortNF after the ShortNFOfCharThree step.

Русский

Если b₂ равно 0, то построенная преобразованием CharThreeNF краткая NF после шага ShortNFOfCharThree даёт ShortNF.

LaTeX

$$$hb_2 : W.b_2 = 0 \Rightarrow (W.toCharThreeNF \cdot W).IsShortNF$$$

Lean4

theorem toCharThreeNF_spec_of_b₂_eq_zero (hb₂ : W.b₂ = 0) : (W.toCharThreeNF • W).IsShortNF :=
  by
  rw [toCharThreeNF, toShortNFOfCharThree_a₂, hb₂, div_zero, ← VariableChange.one_def, one_mul]
  exact W.toShortNFOfCharThree_spec hb₂

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