Commit 2023-07-27 07:08 0bcfc2d2

View on Github →

chore: tidy various files (#6158)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Order.lean

added theorem Fintype.prod_strictMono'

deleted theorem Fintype.prod_strict_mono'

Modified Mathlib/Algebra/Group/UniqueProds.lean

Modified Mathlib/Algebra/Module/LinearMap.lean

modified def DistribMulAction.toModuleEnd

modified def IsLinearMap.mk'

Modified Mathlib/Algebra/Quandle.lean

Modified Mathlib/Combinatorics/SetFamily/Shadow.lean

Modified Mathlib/Data/Int/Parity.lean

Modified Mathlib/Data/List/FinRange.lean

Modified Mathlib/Data/Set/Function.lean

Modified Mathlib/Data/Sym/Basic.lean

modified def Sym.equivCongr

added theorem Sym.ofVector_cons

added theorem Sym.ofVector_nil

deleted theorem Sym.of_vector_cons

deleted theorem Sym.of_vector_nil

Modified Mathlib/GroupTheory/Perm/Basic.lean

modified theorem Equiv.mulLeft_mul

modified theorem Equiv.mulRight_mul

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/Order/Filter/Curry.lean

Modified Mathlib/Order/Filter/Prod.lean

Modified Mathlib/Order/Filter/SmallSets.lean

added theorem Filter.eventually_smallSets'

deleted theorem Filter.eventually_small_sets'

Modified Mathlib/Order/OrderIsoNat.lean

added theorem RelEmbedding.coe_natGT

deleted theorem RelEmbedding.coe_natGt

added theorem RelEmbedding.coe_natLT

deleted theorem RelEmbedding.coe_natLt

added def RelEmbedding.natGT

deleted def RelEmbedding.natGt

added def RelEmbedding.natLT

deleted def RelEmbedding.natLt

Modified Mathlib/Topology/LocallyFinite.lean