Commit 2025-04-12 15:38 39b008d1

View on Github →

feat(NumberTheory/Divisors): Define Nat.divisorsAntidiagonalList (#22977) This PR defines Nat.divisorsAntidiagonalList and proves a couple of basic results. This will be used in #21915 (adds a simproc to compute Nat.divisorsAntidiagonal and Int.divisorsAntidiagonal)

Estimated changes

Modified Mathlib/Data/Finset/Image.lean

added theorem List.toFinset_filterMap

Modified Mathlib/Data/List/Basic.lean

added theorem List.left_le_of_mem_range'

added theorem List.perm_reverse

added theorem List.range'_0

added theorem List.reverse_perm'

Modified Mathlib/Data/List/Pairwise.lean

Modified Mathlib/Data/List/Sort.lean

added theorem List.Sorted.filterMap

added theorem List.sorted_le_range'

added theorem List.sorted_le_replicate

added theorem List.sorted_lt_range'

added theorem List.sorted_replicate

Modified Mathlib/Data/Nat/Init.lean

Modified Mathlib/NumberTheory/Divisors.lean

added def Nat.divisorsAntidiagonalList

added theorem Nat.divisorsAntidiagonalList_one

added theorem Nat.divisorsAntidiagonalList_zero

added theorem Nat.mem_divisorsAntidiagonalList

added theorem Nat.nodup_divisorsAntidiagonalList

added theorem Nat.reverse_divisorsAntidiagonalList

added theorem Nat.sorted_divisorsAntidiagonalList_fst

added theorem Nat.sorted_divisorsAntidiagonalList_snd

added theorem Nat.swap_mem_divisorsAntidiagonalList

added theorem Nat.toFinset_divisorsAntidiagonalList

added theorem Nat.val_divisorsAntidiagonal

Modified Mathlib/Order/Interval/Finset/Nat.lean

added theorem List.toFinset_range'_1

added theorem List.toFinset_range'_1_1