Commit 2025-08-21 08:00 d940994d

View on Github →

feat(NumberTheory/Divisors): add divisorAntidiagonal equivalence. (#27837)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean

added def divisorsAntidiagonalFactors

added theorem divisorsAntidiagonalFactors_eq

added theorem divisorsAntidiagonalFactors_one

added def sigmaAntidiagonalEquivProd

added theorem sigmaAntidiagonalEquivProd_symm_apply_fst

added theorem sigmaAntidiagonalEquivProd_symm_apply_snd