Theorems · Inductive type · combinatorics
Finset.HasAntidiagonal
(A : Type u_1) → [AddMonoid A] → Type u_1
The class of additive monoids with an antidiagonal.
- Defined in
- Mathlib.Algebra.Order.Antidiag.Prod
- Cited by
- 48 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- AddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement · cited by 2,864
Cited by62
Results whose statement or proof uses this declaration.
- Finset.HasAntidiagonal.antidiagonalstatement and proof · cited by 218
- Finset.HasAntidiagonal.mem_antidiagonalstatement and proof · cited by 51
- Finset.finsuppAntidiagstatement and proof · cited by 25
- Finset.piAntidiagstatement and proof · cited by 19
- Finset.HasAntidiagonal.antidiagonal_zerostatement and proof · cited by 8
- Finset.HasAntidiagonal.antidiagonal.fst_lestatement and proof · cited by 6
- Finset.HasAntidiagonal.sigmaAntidiagonalEquivProdstatement and proof · cited by 5
- Finset.HasAntidiagonal.antidiagonal_congrstatement and proof · cited by 4
- Finset.HasAntidiagonal.map_swap_antidiagonalstatement and proof · cited by 4
- summable_sum_mul_antidiagonal_of_summable_mulstatement and proof · cited by 3
- Finset.HasAntidiagonal.map_prodComm_antidiagonalstatement and proof · cited by 3
- Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonalstatement and proof · cited by 3