Commit 2023-02-04 19:53 a347ef63

View on Github →

chore: tidy various files (#2056)

Estimated changes

Modified Mathlib/Data/Finsupp/Defs.lean

modified def Finsupp.embDomain.addMonoidHom

modified def Finsupp.embDomain

modified def Finsupp.equivFunOnFinite

modified def Finsupp.eraseAddHom

modified def Finsupp.update

Modified Mathlib/Data/Finsupp/Multiset.lean

modified def Finsupp.orderIsoMultiset

modified def Finsupp.toMultiset

Modified Mathlib/Data/Finsupp/ToDfinsupp.lean

modified def Finsupp.toDfinsupp

Modified Mathlib/Data/Int/Range.lean

Modified Mathlib/Data/List/MinMax.lean

added theorem List.argAux_self

deleted theorem List.arg_aux_self

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/Range.lean

added theorem List.get?_range

added theorem List.nthLe_range'

deleted theorem List.nth_le_range'

deleted theorem List.nth_range

modified theorem List.range'_eq_map_range

Modified Mathlib/Data/Multiset/Powerset.lean

modified theorem Multiset.powerset_aux'_perm

modified theorem Multiset.revzip_powersetAux'

modified theorem Multiset.revzip_powersetAux

Modified Mathlib/Data/Set/Function.lean

Modified Mathlib/Data/SetLike/Fintype.lean

Modified Mathlib/Topology/Algebra/Constructions.lean

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

added theorem UniformSpace.secondCountable_of_separable

deleted theorem UniformSpace.second_countable_of_separable