Commit 2023-06-16 02:09 62d90431

View on Github →

chore: tidy various files (#5104)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Simple.lean

added theorem simple_iff_isSimpleModule'

deleted theorem simple_iff_is_simple_module'

Modified Mathlib/Algebra/Lie/IdealOperations.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean

added theorem AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux

deleted theorem AlgebraicGeometry.StructureSheaf.is_localized_module_toPushforwardStalkAlgHom_aux

Modified Mathlib/Analysis/Calculus/Series.lean

Modified Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean

Modified Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean

Modified Mathlib/CategoryTheory/Preadditive/Schur.lean

Modified Mathlib/FieldTheory/Laurent.lean

Modified Mathlib/GroupTheory/Transfer.lean

added theorem MonoidHom.transferSylow_eq_pow_aux

deleted theorem MonoidHom.transfer_sylow_eq_pow_aux

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/NumberTheory/FermatPsp.lean

Modified Mathlib/Order/Hom/Lattice.lean

modified theorem LatticeHom.withTopWithBot_apply

Modified Mathlib/Probability/ProbabilityMassFunction/Uniform.lean

Modified Mathlib/RingTheory/Bezout.lean

Modified Mathlib/Topology/ContinuousFunction/Ideals.lean

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean

modified def genLoopEquivOfUnique

modified def genLoopHomeoOfIsEmpty

Modified Mathlib/Topology/SubsetProperties.lean