Commit 2024-08-06 05:13 6fdbc7ed

View on Github →

chore: backports for leanprover/lean4#4814 (part 19) (#15434) see https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

Modified Mathlib/GroupTheory/PGroup.lean

modified theorem IsPGroup.card_center_eq_prime_pow

modified theorem IsPGroup.nonempty_fixed_point_of_prime_not_dvd_card

Modified Mathlib/RingTheory/Binomial.lean

modified theorem Ring.smeval_ascPochhammer_int_ofNat

modified theorem Ring.smeval_ascPochhammer_nat_cast

Modified Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

modified theorem DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid

modified theorem DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.unique_irreducible

Modified Mathlib/RingTheory/Filtration.lean

modified theorem Ideal.Filtration.Stable.exists_pow_smul_eq

modified theorem Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

modified theorem MvPolynomial.homogeneousSubmodule_eq_finsupp_supported

modified theorem MvPolynomial.homogeneousSubmodule_mul

modified theorem MvPolynomial.mem_homogeneousSubmodule

Modified Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean

modified theorem Polynomial.IsEisensteinAt.coeff_mem

modified theorem Polynomial.IsEisensteinAt.irreducible

modified theorem Polynomial.IsEisensteinAt.isWeaklyEisensteinAt

modified theorem Polynomial.IsWeaklyEisensteinAt.map

modified theorem Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_aeval_zero_of_monic_mem_map

modified theorem Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

modified theorem IsPrimitiveRoot.eq_orderOf

modified theorem IsPrimitiveRoot.ne_one

modified theorem IsPrimitiveRoot.pow_eq_one_iff_dvd

modified theorem IsPrimitiveRoot.pow_ne_one_of_pos_of_lt

modified theorem IsPrimitiveRoot.pow_of_coprime

modified theorem IsPrimitiveRoot.sub_one_ne_zero

Modified Mathlib/Topology/Sequences.lean

modified theorem SequentialSpace.coinduced