Commit 2024-08-20 08:16 ad5fca8f

View on Github →

chore: split off Defs from Padics/PadicVal (#15020) Split NumberTheory/Padics/PadicVal.lean into minimal PadicVal/Defs that suffices for import in Factorization/Defs and NumberTheory/Multiplicity, and PadicVal/Basic.

Estimated changes

Modified Mathlib.lean

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

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

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/GroupTheory/CommutingProbability.lean

Modified Mathlib/GroupTheory/Exponent.lean

Modified Mathlib/NumberTheory/Multiplicity.lean

Modified Mathlib/NumberTheory/Padics/PadicNorm.lean

Renamed Mathlib/NumberTheory/Padics/PadicVal.lean to Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

deleted theorem le_multiplicity_iff_replicate_subperm_primeFactorsList

deleted theorem le_padicValNat_iff_replicate_subperm_primeFactorsList

deleted theorem padicValNat.eq_zero_iff

deleted def padicValNat

deleted theorem padicValNat_def'

deleted theorem padicValNat_def

Created Mathlib/NumberTheory/Padics/PadicVal/Defs.lean

added theorem le_multiplicity_iff_replicate_subperm_primeFactorsList

added theorem le_padicValNat_iff_replicate_subperm_primeFactorsList

added theorem padicValNat.eq_zero_iff

added def padicValNat

added theorem padicValNat_def'

added theorem padicValNat_def

Modified Mathlib/NumberTheory/SumTwoSquares.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean

Modified test/MaxPowDiv.lean