Commit 2023-02-23 12:36 c2182a74

View on Github →

chore: tidy various files (#2462)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/BigOperators/Intervals.lean

Modified Mathlib/Algebra/Module/Equiv.lean

modified def LinearEquiv.automorphismGroup.toLinearMapMonoidHom

Modified Mathlib/CategoryTheory/DiscreteCategory.lean

modified def CategoryTheory.Discrete.equivOfEquivalence

modified def CategoryTheory.Discrete.equivalence

modified def CategoryTheory.Discrete.functor

modified def CategoryTheory.discreteEquiv

Modified Mathlib/Data/Finset/Pointwise.lean

Modified Mathlib/Data/Finsupp/Order.lean

modified def Finsupp.orderEmbeddingToFun

Modified Mathlib/Data/Finsupp/Pointwise.lean

Modified Mathlib/Data/Rat/NNRat.lean

added theorem NNRat.coe_natCast

deleted theorem NNRat.coe_nat_cast

Modified Mathlib/Dynamics/Flow.lean

Modified Mathlib/Init/Data/Quot.lean

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/Order/Filter/Ultrafilter.lean

Modified Mathlib/Order/SuccPred/LinearLocallyFinite.lean

Modified Mathlib/SetTheory/Lists.lean

modified theorem Lists'.cons_subset

modified theorem Lists'.mem_of_subset'

modified theorem Lists'.subset_nil

modified theorem Lists.Equiv.trans

added theorem Lists.isList_of_mem

deleted theorem Lists.is_list_of_mem