count_finsuppProd — Mathlib

English

A tautology about equality of nested if-then expressions: Eq (Eq (ite p x y) y) (p → Eq x y).

Русский

Тавтологическое утверждение про равенство вложенных выражений вида if-then: Eq (Eq (ite p x y) y) (p → Eq x y).

LaTeX

$$$$ \\mathrm{Eq}\\bigl(\\mathrm{Eq}(\\mathrm{ite}\\,p\\,x\\,y)\\,y\\bigr)\\;\\bigl(p \\to \\mathrm{Eq}\\,x\\,y\\bigr). $$$$

Lean4

theorem count_finsuppProd (exps : HeightOneSpectrum R →₀ ℤ) :
    count K v (exps.prod (HeightOneSpectrum.asIdeal · ^ ·)) = exps v :=
  by
  rw [Finsupp.prod, count_prod]
  ·
    classical
      simp only [count_zpow, count_maximal, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq', exps.mem_support_iff, ne_eq,
      ite_not, ite_eq_right_iff, @eq_comm ℤ 0, imp_self]
  · exact fun v hv ↦ zpow_ne_zero _ (coeIdeal_ne_zero.mpr v.ne_bot)

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