Theorems · Theorem · combinatorics

Finset.HasMulAntidiagonal.mulAntidiagonal_congr

∀ {A : Type u_1} [inst : CancelMonoid A] [inst_1 : Finset.HasMulAntidiagonal A] {p q : A × A} {n : A},
  p ∈ Finset.HasMulAntidiagonal.mulAntidiagonal n →
    q ∈ Finset.HasMulAntidiagonal.mulAntidiagonal n → (p = q ↔ p.1 = q.1)

A point in the mulAntidiagonal is determined by its first coordinate. See also Finset.mulAntidiagonal_congr'.

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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

Finsetstatement · cited by 13,712
CancelMonoidstatement and proof · cited by 20
Finset.HasMulAntidiagonal.mulAntidiagonalstatement and proof · cited by 17
Finset.HasMulAntidiagonalstatement and proof · cited by 16
mul_right_injproof · cited by 11
Finset.HasMulAntidiagonal.mem_mulAntidiagonalproof · cited by 3

Cited by2

Results whose statement or proof uses this declaration.

Finset.HasMulAntidiagonal.mulAntidiagonal_subtype_extproof · cited by 1
Finset.HasMulAntidiagonal.mulAntidiagonal_congr'proof · cited by 0