Commit 2023-12-04 07:49 90d520aa

View on Github →

chore: split Algebra.CharP.Basic, reduce imports in RingTheory.Multiplicity (#8637) This was adding unnecessary imports to Data.ZMod.Basic.

Estimated changes

Modified Counterexamples/CharPZeroNeCharZero.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/CharP/Basic.lean

deleted theorem CharP.pow_prime_pow_mul_eq_one_iff

deleted theorem frobenius_inj

deleted theorem isSquare_of_charTwo'

Modified Mathlib/Algebra/CharP/Quotient.lean

Created Mathlib/Algebra/CharP/Reduced.lean

added theorem CharP.pow_prime_pow_mul_eq_one_iff

added theorem frobenius_inj

added theorem isSquare_of_charTwo'

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/FieldTheory/Perfect.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

Modified Mathlib/RingTheory/Multiplicity.lean

deleted theorem multiplicity.addValuation_apply

Created Mathlib/RingTheory/Valuation/PrimeMultiplicity.lean

added theorem multiplicity.addValuation_apply