card_support_eraseLead — Mathlib

English

For any nonzero polynomial f, the cardinality of eraseLead f .support equals the cardinality of f .support minus one.

Русский

Для любого ненулевого многочлена f кардинал поддержки eraseLead(f) равен кардиналу поддержки f минус одна.

LaTeX

$$$#(eraseLead f).\,support = #f.\,support - 1$$$

Lean4

@[simp]
theorem card_support_eraseLead : #f.eraseLead.support = #f.support - 1 :=
  by
  by_cases hf : f = 0
  · rw [hf, eraseLead_zero, support_zero, card_empty]
  · rw [← card_support_eraseLead_add_one hf, add_tsub_cancel_right]

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