Commit 2023-05-26 17:27 8214f469

View on Github →

chore: tidy various files (#4304)

Estimated changes

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

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

Modified Mathlib/Algebra/Module/Bimodule.lean

Modified Mathlib/Analysis/Complex/Basic.lean

added theorem Complex.restrictScalars_one_smulRight'

deleted theorem Complex.restrictScalars_one_smul_right'

Modified Mathlib/CategoryTheory/Category/Preorder.lean

added def CategoryTheory.opHomOfLE

deleted def CategoryTheory.opHomOfLe

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

Modified Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean

Modified Mathlib/Computability/Partrec.lean

Modified Mathlib/Data/Fin/VecNotation.lean

Modified Mathlib/GroupTheory/Congruence.lean

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

Modified Mathlib/MeasureTheory/Function/SpecialFunctions/IsROrC.lean

added theorem IsROrC.measurable_ofReal

deleted theorem IsROrC.measurable_of_real

Modified Mathlib/MeasureTheory/Measure/OuterMeasure.lean

added theorem MeasureTheory.OuterMeasure.le_boundedBy'

deleted theorem MeasureTheory.OuterMeasure.le_bounded_by'

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean

deleted theorem ZMod.test

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

added theorem Polynomial.mem_ker_modByMonic

deleted theorem Polynomial.mem_ker_mod_by_monic

Modified Mathlib/RingTheory/PolynomialAlgebra.lean

added theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_1

added theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2

deleted theorem PolyEquivTensor.to_fun_linear_mul_tmul_mul_aux_1

deleted theorem PolyEquivTensor.to_fun_linear_mul_tmul_mul_aux_2

Modified Mathlib/RingTheory/QuotientNilpotent.lean

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

Modified Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean

Modified Mathlib/Topology/MetricSpace/PartitionOfUnity.lean

Modified Mathlib/Topology/PathConnected.lean

Modified Mathlib/Topology/Sheaves/PresheafOfFunctions.lean