card_support_eraseLead_add_one — Mathlib

English

If f ≠ 0, then the support of eraseLead f is one less than the support of f.

Русский

Если f ≠ 0, то поддержка eraseLead f на единицу меньше поддержки f.

LaTeX

$$ #(eraseLead f).support + 1 = #f.support$$

Lean4

theorem card_support_eraseLead_add_one (h : f ≠ 0) : #f.eraseLead.support + 1 = #f.support :=
  by
  set c := #f.support with hc
  cases h₁ : c
  case zero =>
    by_contra
    exact h (card_support_eq_zero.mp h₁)
  case succ =>
    rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero h), ← hc, h₁]
    rfl

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