Commit 2024-04-28 07:15 51a6e529

View on Github →

chore: reduce proof dependencies for Nat.factors_count_eq (#12105) This is a bit longer, partially duplicating the argument from UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors, but it means we no longer need to depend on RingTheory.Int.Basic at this point. The other added lemmas seem useful regardless.

Estimated changes

Modified Mathlib/Algebra/BigOperators/List/Lemmas.lean

added theorem List.Sublist.prod_dvd_prod

Modified Mathlib/Algebra/Category/GroupCat/Injective.lean

Modified Mathlib/Data/List/Lex.lean

added theorem List.nil_le

Modified Mathlib/Data/List/Perm.lean

added theorem List.subperm_nil

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

Modified Mathlib/Data/Nat/Factors.lean

added theorem Nat.replicate_subperm_factors_iff

Modified Mathlib/NumberTheory/Padics/PadicVal.lean

added theorem le_multiplicity_iff_replicate_subperm_factors

added theorem le_padicValNat_iff_replicate_subperm_factors