Theorems · Definition · combinatorics

Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd

{A : Type u_1} →
  [inst : AddMonoid A] →
    [inst_1 : Finset.HasAntidiagonal A] → (n : A) × ↥(Finset.HasAntidiagonal.antidiagonal n) ≃ A × A

The disjoint union of antidiagonals Σ (n : A), antidiagonal 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: 5 results in Mathlib
Foundations: Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddMonoid Finset.HasAntidiagonal

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
AddMonoidstatement and proof · cited by 2,864
Finset.HasAntidiagonal.antidiagonalstatement and proof · cited by 218
Finset.HasAntidiagonalstatement and proof · cited by 48

Cited by5

Results whose statement or proof uses this declaration.

Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonalproof · cited by 3
summable_mul_prod_iff_summable_mul_sigma_antidiagonalproof · cited by 2
Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd_applystatement and proof · cited by 0
Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd_symm_apply_fststatement and proof · cited by 0
Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd_symm_apply_snd_coestatement and proof · cited by 0