Structures · Algebra
Finset.HasMulAntidiagonal
The class of (multiplicative) monoids with a mulAntidiagonal.
- Defined in
- Mathlib.Algebra.Order.Antidiag.Prod
- Shape
- One type argument · adds mulAntidiagonal, mem_mulAntidiagonal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- Finset.HasMulAntidiagonal.mulAntidiagonal
- Finset.HasMulAntidiagonal.mem_mulAntidiagonal
- Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd
- Finset.HasMulAntidiagonal.mulAntidiagonal_congr
- Finset.HasMulAntidiagonal.map_prodComm_mulAntidiagonal
- Finset.HasMulAntidiagonal.swap_mem_mulAntidiagonal
- Finset.HasMulAntidiagonal.mulAntidiagonal_subtype_ext
- Finset.HasMulAntidiagonal.mulAntidiagonal_congr'
- Finset.HasMulAntidiagonal.mulAntidiagonal.fst_le
- Finset.HasMulAntidiagonal.map_swap_mulAntidiagonal
- Finset.HasMulAntidiagonal.mulAntidiagonal.snd_le
- Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd_symm_apply_fst
- Finset.HasMulAntidiagonal.mulAntidiagonal_one
- Finset.HasMulAntidiagonal.nonempty_antidiagonal
- Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd_apply
- Finset.HasMulAntidiagonal.congr
- Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd_symm_apply_snd_coe
- Finset.HasMulAntidiagonal.mulAntidiagonal_subtype_ext_iff
Ancestors0
No ancestors.