Commit 2023-07-26 17:00 415165ea

View on Github →

chore: tidy various files (#5999)

Estimated changes

Modified Mathlib/Algebra/GCDMonoid/Finset.lean

modified theorem Finset.lcm_congr

Modified Mathlib/Algebra/Hom/Centroid.lean

added theorem CentroidHom.toFun_eq_coe

Modified Mathlib/Algebra/Order/Kleene.lean

Modified Mathlib/Algebra/Ring/Prod.lean

added theorem RingEquiv.coe_prodComm

added theorem RingEquiv.coe_prodComm_symm

deleted theorem RingEquiv.coe_prod_comm

deleted theorem RingEquiv.coe_prod_comm_symm

added theorem RingEquiv.fst_comp_coe_prodComm

deleted theorem RingEquiv.fst_comp_coe_prod_comm

added theorem RingEquiv.snd_comp_coe_prodComm

deleted theorem RingEquiv.snd_comp_coe_prod_comm

Modified Mathlib/Analysis/Convex/StrictConvexSpace.lean

deleted theorem StrictConvexSpace.ofNormAdd

deleted theorem StrictConvexSpace.ofNormAddNeTwo

deleted theorem StrictConvexSpace.ofNormComboLtOne

deleted theorem StrictConvexSpace.ofNormComboNeOne

deleted theorem StrictConvexSpace.ofPairwiseSphereNormNeTwo

deleted theorem StrictConvexSpace.ofStrictConvexClosedUnitBall

added theorem StrictConvexSpace.of_norm_add

added theorem StrictConvexSpace.of_norm_add_ne_two

added theorem StrictConvexSpace.of_norm_combo_lt_one

added theorem StrictConvexSpace.of_norm_combo_ne_one

added theorem StrictConvexSpace.of_pairwise_sphere_norm_ne_two

added theorem StrictConvexSpace.of_strictConvex_closed_unit_ball

Modified Mathlib/Analysis/Convex/Uniform.lean

Modified Mathlib/Analysis/Normed/Field/Basic.lean

Modified Mathlib/CategoryTheory/Groupoid.lean

modified def CategoryTheory.Groupoid.isoEquivHom

modified def CategoryTheory.Groupoid.ofHomUnique

Modified Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean

Modified Mathlib/CategoryTheory/Opposites.lean

modified def CategoryTheory.Functor.leftOpRightOpEquiv

modified def CategoryTheory.Functor.opUnopEquiv

modified def CategoryTheory.Iso.unop

modified def CategoryTheory.isoOpEquiv

modified def CategoryTheory.opEquiv

Modified Mathlib/Computability/Language.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/RingTheory/Localization/AtPrime.lean

Modified Mathlib/Topology/Algebra/MulAction.lean