Theorems · Theorem · number theory

Finset.Nat.antidiagonal_succ

∀ (n : ℕ),
  Finset.HasAntidiagonal.antidiagonal (n + 1) =
    Finset.cons (0, n + 1)
      (Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ))
        (Finset.HasAntidiagonal.antidiagonal n))
      ⋯

Defined in: Mathlib.Data.Finset.NatAntidiagonal
Cited by: 2 results in Mathlib
Foundations: Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites14

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

Finsetstatement · cited by 13,712
Multisetproof · cited by 2,627
Finset.mapstatement · cited by 747
Finset.valproof · cited by 438
Multiset.consproof · cited by 313
Finset.consstatement · cited by 221
Finset.HasAntidiagonal.antidiagonalstatement and proof · cited by 218
Finset.eq_of_veqproof · cited by 45
Function.Embedding.reflstatement and proof · cited by 29
Function.Embedding.prodMapstatement and proof · cited by 23
Nat.succ_injectivestatement and proof · cited by 14
Finset.map_valproof · cited by 7

Cited by2

Results whose statement or proof uses this declaration.

Finset.Nat.prod_antidiagonal_succproof · cited by 2
Finset.Nat.antidiagonal_succ_succ'proof · cited by 1