Commit 2025-01-10 04:57 2bd5a6b1

View on Github →

chore: cleanup imports in PrimePow/Divisors (#20626) Moves a theorem to reduce the NumberTheory -> Algebra imports.

Estimated changes

Modified Mathlib/Algebra/IsPrimePow.lean

deleted theorem Nat.disjoint_divisors_filter_isPrimePow

Modified Mathlib/Data/Nat/Factorization/PrimePow.lean

Modified Mathlib/NumberTheory/Divisors.lean

added theorem Nat.disjoint_divisors_filter_isPrimePow