coeff_of_not_mem_CNF — Mathlib

English

If e does not appear among the exponents of CNF(b,o), then the coefficient at e is zero.

Русский

Если e не встречается среди показателей CNF(b,o), то коэффициент при e равен 0.

LaTeX

$$$$ e \\notin (CNF(b,o)).map \\text{Prod.fst} \\;\rightarrow\; \\operatorname{coeff}(b,o,e) = 0 $$$$

Lean4

theorem coeff_of_not_mem_CNF {b o e : Ordinal} (h : e ∉ (CNF b o).map Prod.fst) : coeff b o e = 0 :=
  by
  rw [coeff, lookupFinsupp_apply, lookup_eq_none.2, Option.getD_none]
  simp_all [List.keys]

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