Commit 2023-09-12 22:27 0c1c834a

View on Github →

feat(NumberTheory/Divisors): Two lemmas about filtering by divisibility (#7084) Add lemmas about filtering the Finsets of divisors or factors by divisibility. These two results came up while developing API for the Finset of tuples with a fixed product n.

Estimated changes

Modified Mathlib/NumberTheory/Divisors.lean

added theorem Nat.divisors_filter_dvd_of_dvd

added theorem Nat.prime_divisors_filter_dvd_of_dvd