Theorems · Theorem · number theory

Int.divisorsAntidiag_neg_natCast

∀ (n : ℕ),
  (-↑n).divisorsAntidiag =
    (Finset.map (Nat.castEmbedding.prodMap (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))))
          n.divisorsAntidiagonal).disjUnion
      (Finset.map ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap Nat.castEmbedding)
        n.divisorsAntidiagonal)
      ⋯

Defined in: Mathlib.NumberTheory.Divisors
Cited by: 0 results in Mathlib
Foundations: Depth 63 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.

Cites10

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

Finsetstatement · cited by 13,712
Finset.mapstatement · cited by 747
Equiv.toEmbeddingstatement · cited by 254
Function.Embedding.transstatement · cited by 83
Nat.divisorsAntidiagonalstatement · cited by 61
Finset.disjUnionstatement · cited by 55
Equiv.negstatement · cited by 53
Nat.castEmbeddingstatement · cited by 29
Function.Embedding.prodMapstatement · cited by 23
Int.divisorsAntidiagstatement and proof · cited by 17

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.