Theorems · Inductive type · combinatorics
Finset.HasMulAntidiagonal
(A : Type u_1) → [Monoid A] → Type u_1
The class of (multiplicative) monoids with a mulAntidiagonal.
- Defined in
- Mathlib.Algebra.Order.Antidiag.Prod
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Monoid
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.
- Monoidstatement · cited by 3,887
Cited by25
Results whose statement or proof uses this declaration.
- Finset.HasMulAntidiagonal.mulAntidiagonalstatement and proof · cited by 17
- Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProdstatement and proof · cited by 3
- Finset.HasMulAntidiagonal.mem_mulAntidiagonalstatement and proof · cited by 3
- Finset.HasMulAntidiagonal.mulAntidiagonal_congrstatement and proof · cited by 2
- Finset.HasMulAntidiagonal.swap_mem_mulAntidiagonalstatement and proof · cited by 1
- Finset.HasMulAntidiagonal.map_prodComm_mulAntidiagonalstatement and proof · cited by 1
- Finset.HasMulAntidiagonal.mulAntidiagonal_subtype_extstatement and proof · cited by 1
- Finset.HasMulAntidiagonal.noConfusionstatement and proof · cited by 0
- Finset.HasMulAntidiagonal.noConfusionTypestatement and proof · cited by 0
- Finset.HasMulAntidiagonal.nonempty_antidiagonalstatement and proof · cited by 0
- Finset.HasMulAntidiagonal.recOnstatement and proof · cited by 0
- Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd_applystatement and proof · cited by 0