Commit 2023-06-24 18:07 ff656fa9

View on Github →

chore: tidy various files (#5449)

Estimated changes

Modified Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

Modified Mathlib/Algebra/Category/Mon/FilteredColimits.lean

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

Modified Mathlib/Analysis/Calculus/BumpFunctionFindim.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean

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

Modified Mathlib/Data/Nat/PartENat.lean

Modified Mathlib/FieldTheory/Finite/GaloisField.lean

added theorem GaloisField.splits_X_pow_card_sub_X

deleted theorem GaloisField.splits_x_pow_card_sub_x

deleted theorem GaloisField.splits_zMod_x_pow_sub_x

added theorem GaloisField.splits_zmod_X_pow_sub_X

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

added theorem IsIntegrallyClosed.minpoly.unique

deleted theorem minpoly.IsIntegrallyClosed.Minpoly.unique

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/NumberTheory/ADEInequality.lean

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

added theorem IsCyclotomicExtension.neZero'

deleted theorem IsCyclotomicExtension.ne_zero'

Modified Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

Modified Mathlib/NumberTheory/LegendreSymbol/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

Modified Mathlib/Probability/Process/Filtration.lean

Modified Mathlib/RingTheory/Ideal/Norm.lean

Modified Mathlib/RingTheory/Norm.lean

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

added theorem IsPrimitiveRoot.neZero'

deleted theorem IsPrimitiveRoot.ne_zero'

Modified Mathlib/RingTheory/SimpleModule.lean

Modified Mathlib/Topology/MetricSpace/MetrizableUniformity.lean

Modified Mathlib/Topology/Order/Basic.lean

Modified Mathlib/Topology/Perfect.lean