Theorems · Theorem · combinatorics

Finset.finsuppAntidiag_zero

∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : DecidableEq μ] [inst_2 : AddCommMonoid μ]
  [inst_3 : PartialOrder μ] [CanonicallyOrderedAdd μ] [inst_5 : Finset.HasAntidiagonal μ] (s : Finset ι),
  s.finsuppAntidiag 0 = {0}

Defined in: Mathlib.Algebra.Order.Antidiag.Finsupp
Cited by: 0 results in Mathlib
Foundations: Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq DecidableEq AddCommMonoid PartialOrder CanonicallyOrderedAdd Finset.HasAntidiagonal

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites18

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Finsetstatement and proof · cited by 13,712
AddCommMonoidstatement and proof · cited by 12,281
PartialOrderstatement and proof · cited by 6,410
Finsuppstatement and proof · cited by 5,255
Finset.filterproof · cited by 949
Finset.mapproof · cited by 747
Finset.extproof · cited by 565
CanonicallyOrderedAddstatement and proof · cited by 229
Finset.attachproof · cited by 168
Finset.filter_congrproof · cited by 167
Finset.HasAntidiagonalstatement and proof · cited by 48

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.