Commit 2023-09-14 06:57 cdbcc219

View on Github →

chore: tidy various files (#7137)

Estimated changes

Modified Mathlib/Algebra/Algebra/Unitization.lean

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

deleted theorem MagmaCat.MulEquiv_coe_eq

added theorem MagmaCat.mulEquiv_coe_eq

deleted theorem SemigroupCat.MulEquiv_coe_eq

added theorem SemigroupCat.mulEquiv_coe_eq

Modified Mathlib/Algebra/Star/Order.lean

added def StarOrderedRing.ofLEIff

deleted def StarOrderedRing.ofLeIff

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

deleted theorem tsum_geometric_nNReal

added theorem tsum_geometric_nnreal

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

Modified Mathlib/Data/Bundle.lean

Modified Mathlib/FieldTheory/RatFunc.lean

added theorem RatFunc.liftOn_condition_of_liftOn'_condition

deleted theorem RatFunc.lift_on_condition_of_lift_on'_condition

modified theorem RatFunc.mul_inv_cancel

Modified Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean

Modified Mathlib/Logic/Equiv/TransferInstance.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/RingTheory/FractionalIdeal.lean

Modified Mathlib/Topology/Order/UpperLowerSetTopology.lean

deleted theorem WithLowerSetTopology.IsLowerSet_toLowerSet_preimage

added theorem WithLowerSetTopology.isLowerSet_toLowerSet_preimage

deleted theorem WithUpperSetTopology.IsUpperSet_toUpperSet_preimage

added theorem WithUpperSetTopology.isUpperSet_toUpperSet_preimage