Theorems · Definition · combinatorics

Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd

{A : Type u_1} →
  [inst : Monoid A] →
    [inst_1 : Finset.HasMulAntidiagonal A] → (n : A) × ↥(Finset.HasMulAntidiagonal.mulAntidiagonal n) ≃ A × A

The disjoint union of mulAntidiagonals Σ (n : A), mulAntidiagonal n is equivalent to the product A × A. This is such an equivalence, obtained by mapping (n, (k, l)) to (k, l).

Defined in: Mathlib.Algebra.Order.Antidiag.Prod
Cited by: 3 results in Mathlib
Foundations: Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Monoid Finset.HasMulAntidiagonal

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Finsetstatement · cited by 13,712
Equivstatement · cited by 8,337
Monoidstatement and proof · cited by 3,887
Finset.HasMulAntidiagonal.mulAntidiagonalstatement and proof · cited by 17
Finset.HasMulAntidiagonalstatement and proof · cited by 16

Cited by3

Results whose statement or proof uses this declaration.

Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd_applystatement and proof · cited by 0
Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd_symm_apply_fststatement and proof · cited by 0
Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd_symm_apply_snd_coestatement and proof · cited by 0