Commit 2023-04-10 18:08 5cedfb5e

View on Github →

chore: tidy various files (#3358)

Estimated changes

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

modified def MulEquiv.toCommGroupCatIso

modified def mulEquivIsoCommGroupIso

Modified Mathlib/Algebra/GroupPower/Order.lean

Modified Mathlib/CategoryTheory/Limits/Lattice.lean

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

Modified Mathlib/CategoryTheory/Localization/Opposite.lean

Modified Mathlib/CategoryTheory/Shift/Basic.lean

added theorem CategoryTheory.shiftComm'

added theorem CategoryTheory.shiftZero'

deleted theorem CategoryTheory.shift_comm'

deleted theorem CategoryTheory.shift_zero'

Modified Mathlib/CategoryTheory/Sites/Pretopology.lean

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

Modified Mathlib/Data/List/Intervals.lean

Modified Mathlib/Data/Matrix/DualNumber.lean

Modified Mathlib/Data/Multiset/Pi.lean

Modified Mathlib/Data/MvPolynomial/CommRing.lean

Modified Mathlib/Data/Nat/Multiplicity.lean

Modified Mathlib/ModelTheory/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

modified def Ideal.ofPolynomial

added theorem Polynomial.coeff_toSubring'

deleted theorem Polynomial.coeff_to_subring'

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

Modified Mathlib/Topology/PathConnected.lean

modified def Path.cast

modified def Path.ofLine

modified def Path.trans

added def Path.truncateOfLE

deleted def Path.truncateOfLe

Modified Mathlib/Topology/Semicontinuous.lean

deleted theorem lowerSemicontinuousAt_bsupr

added theorem lowerSemicontinuousAt_bsupᵢ

deleted theorem lowerSemicontinuousAt_csupr

added theorem lowerSemicontinuousAt_csupᵢ

deleted theorem lowerSemicontinuousOn_bsupr

added theorem lowerSemicontinuousOn_bsupᵢ

deleted theorem lowerSemicontinuousOn_csupr

added theorem lowerSemicontinuousOn_csupᵢ

deleted theorem lowerSemicontinuousWithinAt_bsupr

added theorem lowerSemicontinuousWithinAt_bsupᵢ

deleted theorem lowerSemicontinuousWithinAt_csupr

added theorem lowerSemicontinuousWithinAt_csupᵢ

deleted theorem lowerSemicontinuous_bsupr

added theorem lowerSemicontinuous_bsupᵢ

deleted theorem lowerSemicontinuous_csupr

added theorem lowerSemicontinuous_csupᵢ

deleted theorem upperSemicontinuousAt_binfi

added theorem upperSemicontinuousAt_binfᵢ

deleted theorem upperSemicontinuousAt_cinfi

added theorem upperSemicontinuousAt_cinfᵢ

deleted theorem upperSemicontinuousOn_binfi

added theorem upperSemicontinuousOn_binfᵢ

deleted theorem upperSemicontinuousOn_cinfi

added theorem upperSemicontinuousOn_cinfᵢ

deleted theorem upperSemicontinuousWithinAt_binfi

added theorem upperSemicontinuousWithinAt_binfᵢ

deleted theorem upperSemicontinuousWithinAt_cinfi

added theorem upperSemicontinuousWithinAt_cinfᵢ

deleted theorem upperSemicontinuous_binfi

added theorem upperSemicontinuous_binfᵢ

deleted theorem upperSemicontinuous_cinfi

added theorem upperSemicontinuous_cinfᵢ