Structures · Algebra
Finset.HasAntidiagonal
The class of additive monoids with an antidiagonal.
- Defined in
- Mathlib.Algebra.Order.Antidiag.Prod
- Shape
- One type argument · adds antidiagonal, mem_antidiagonal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Nat
- Finsupp
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by56
- Finset.HasAntidiagonal.antidiagonal
- Finset.HasAntidiagonal.mem_antidiagonal
- Finset.finsuppAntidiag
- Finset.piAntidiag
- Finset.HasAntidiagonal.antidiagonal_zero
- Finset.HasAntidiagonal.antidiagonal.fst_le
- Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd
- Finset.HasAntidiagonal.antidiagonal_congr
- Finset.HasAntidiagonal.map_swap_antidiagonal
- summable_sum_mul_antidiagonal_of_summable_mul
- Finset.HasAntidiagonal.antidiagonal.snd_le
- Finset.pairwiseDisjoint_piAntidiag_map_addRightEmbedding
- Finset.HasAntidiagonal.map_prodComm_antidiagonal
- Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal
- Finset.finsuppAntidiagEquivSubtype
- Finset.piAntidiag_zero
- summable_mul_prod_iff_summable_mul_sigma_antidiagonal
- Finset.HasAntidiagonal.filter_fst_eq_antidiagonal
- Finset.mem_finsuppAntidiag
- Finset.piAntidiag_empty_of_ne_zero
- Finset.piAntidiag_cons
- Finset.HasAntidiagonal.nonempty_antidiagonal
- Finset.mem_finsuppAntidiag_insert
- Finset.mapRange_finsuppAntidiag_eq
- Finset.mapRange_finsuppAntidiag_subset
- Finset.HasAntidiagonal.tendsto_sup'_antidiagonal_cofinite
- Finset.finsuppAntidiagEquivSubtype_apply_coe
- Finset.HasAntidiagonal.antidiagonal_congr'
- Finset.mem_piAntidiag
- Finset.finsuppAntidiag_mono
- Finset.finAntidiagonal.aux
- Finset.finsuppAntidiag_empty_zero
- Finset.HasAntidiagonal.filter_snd_eq_antidiagonal
- Finset.HasAntidiagonal.antidiagonal_subtype_ext
- Finset.finsuppAntidiag_insert
- MvPowerSeries.tendsto_antidiagonal
- Finset.piAntidiag_empty_zero
- Finset.finsuppAntidiagEquivSubtype_symm_apply_coe
- Finset.finAntidiagonal
- Finset.finsuppAntidiag_empty_of_ne_zero
- Finset.finsuppAntidiag_empty
- Finset.HasAntidiagonal.swap_mem_antidiagonal
- Finset.finsuppAntidiag_zero
- Finset.piAntidiag_empty
- Finset.piAntidiag_insert
- Finset.mem_finsuppAntidiag'
- Finset.HasMulAntidiagonal.mem_mulAntidiagonal_ofAdd_iff_toAdd_mem_antidiagonal
- Finset.HasMulAntidiagonal.instMultiplicative
- Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd_symm_apply_fst
- Finset.HasAntidiagonal.congr
Ancestors0
No ancestors.