Commit 2023-05-16 13:10 3450d097

View on Github →

chore: tidy various files (#4003)

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Basic.lean

Modified Mathlib/Algebra/Ring/BooleanRing.lean

Modified Mathlib/Analysis/Normed/Group/Quotient.lean

Modified Mathlib/Analysis/Seminorm.lean

added def Seminorm.ofSMulLE

deleted def Seminorm.ofSMulLe

Modified Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean

Modified Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.lean

added theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj'

deleted theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditive_coyoneda_obj'

Modified Mathlib/CategoryTheory/Sites/CoverPreserving.lean

Modified Mathlib/CategoryTheory/Sites/DenseSubsite.lean

Modified Mathlib/ModelTheory/Definability.lean

Modified Mathlib/ModelTheory/ElementaryMaps.lean

Modified Mathlib/ModelTheory/FinitelyGenerated.lean

Modified Mathlib/ModelTheory/Order.lean

Modified Mathlib/Topology/Category/Top/OpenNhds.lean

added def TopologicalSpace.OpenNhds.infLELeft

added def TopologicalSpace.OpenNhds.infLERight

deleted def TopologicalSpace.OpenNhds.infLeLeft

deleted def TopologicalSpace.OpenNhds.infLeRight