Commit 2023-03-09 12:59 8c7b65ad

View on Github →

chore: tidy various files (#2742)

Estimated changes

Modified Mathlib/Algebra/DirectSum/Basic.lean

Modified Mathlib/Algebra/Quandle.lean

Modified Mathlib/CategoryTheory/Limits/Cones.lean

modified def CategoryTheory.Limits.Cocone.whisker

modified def CategoryTheory.Limits.Cocones.whiskering

modified def CategoryTheory.Limits.Cocones.whiskeringEquivalence

modified def CategoryTheory.Limits.Cones.postcompose

modified def CategoryTheory.Limits.Cones.postcomposeEquivalence

modified def CategoryTheory.Limits.Cones.whiskering

modified def CategoryTheory.Limits.Cones.whiskeringEquivalence

modified def CategoryTheory.Limits.coconeEquivalenceOpConeOp

modified def CategoryTheory.Limits.coconeLeftOpOfCone

modified def CategoryTheory.Limits.coconeOfConeLeftOp

modified def CategoryTheory.Limits.coconeOfConeRightOp

modified def CategoryTheory.Limits.coconeOfConeUnop

modified def CategoryTheory.Limits.coconeRightOpOfCone

modified def CategoryTheory.Limits.coconeUnopOfCone

modified def CategoryTheory.Limits.coneLeftOpOfCocone

modified def CategoryTheory.Limits.coneOfCoconeLeftOp

modified def CategoryTheory.Limits.coneOfCoconeRightOp

modified def CategoryTheory.Limits.coneOfCoconeUnop

modified def CategoryTheory.Limits.coneRightOpOfCocone

modified def CategoryTheory.Limits.coneUnopOfCocone

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean

modified def CategoryTheory.Functor.mapZeroObject

modified theorem CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object

Modified Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean

modified theorem CategoryTheory.Limits.initialMonoClass_of_disjoint_coproducts

Modified Mathlib/CategoryTheory/Limits/Shapes/FiniteProducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean

Modified Mathlib/CategoryTheory/StructuredArrow.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

deleted theorem SimpleGraph.edgeFinset_sSubset_edgeFinset

added theorem SimpleGraph.edgeFinset_ssubset_edgeFinset

deleted theorem SimpleGraph.edgeSet_sSubset_edgeSet

added theorem SimpleGraph.edgeSet_ssubset_edgeSet

Modified Mathlib/Combinatorics/SimpleGraph/Hasse.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/Option.lean

Modified Mathlib/Data/List/NodupEquivFin.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Nat/Digits.lean

added theorem Nat.ofDigits_modEq'

deleted theorem Nat.ofDigits_modeq'

Modified Mathlib/FieldTheory/Subfield.lean

deleted theorem Subfield.toSubring.subtype_eq_subtype

added theorem Subfield.toSubring_subtype_eq_subtype

Modified Mathlib/Order/Hom/Basic.lean

added theorem OrderEmbedding.coe_ofMapLEIff

deleted theorem OrderEmbedding.coe_ofMapLeIff

added def OrderEmbedding.ofMapLEIff

deleted def OrderEmbedding.ofMapLeIff

Modified Mathlib/Order/JordanHolder.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/Topology/Algebra/GroupCompletion.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Order.lean

added theorem isLUB_hasSum'

deleted theorem isLUB_has_sum'

added theorem le_hasSum'

deleted theorem le_has_sum'

Modified Mathlib/Topology/Algebra/Order/Field.lean

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

added theorem TopologicalRing.of_addGroup_of_nhds_zero

deleted theorem TopologicalRing.of_add_group_of_nhds_zero

Modified Mathlib/Topology/UnitInterval.lean