Commit 2023-08-06 01:46 54997305

View on Github →

chore: tidy various files (#6382)

Estimated changes

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

Modified Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean

Modified Mathlib/Analysis/Calculus/DiffContOnCl.lean

added theorem DiffContOnCl.differentiableAt'

deleted theorem DiffContOnCl.differentiable_at'

Modified Mathlib/Analysis/Calculus/FDeriv/Mul.lean

Modified Mathlib/MeasureTheory/Function/Egorov.lean

added def MeasureTheory.Egorov.notConvergentSeqLTIndex

added theorem MeasureTheory.Egorov.notConvergentSeqLTIndex_spec

deleted def MeasureTheory.Egorov.notConvergentSeqLtIndex

deleted theorem MeasureTheory.Egorov.notConvergentSeqLtIndex_spec

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/IsTensorProduct.lean

added theorem IsBaseChange.algHom_ext'

added theorem IsBaseChange.algHom_ext

deleted theorem IsBaseChange.alg_hom_ext'

deleted theorem IsBaseChange.alg_hom_ext