Commit 2023-01-17 08:03 6fe10b88

View on Github →

chore: tidy various files (#1595)

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

deleted theorem multiplicative_of_IsTotal

added theorem multiplicative_of_isTotal

Modified Mathlib/Algebra/Group/Units.lean

Modified Mathlib/Algebra/PUnitInstances.lean

Modified Mathlib/Data/List/AList.lean

added theorem AList.entries_toAList

deleted theorem AList.entries_to_alist

added theorem AList.lookup_isSome

deleted theorem AList.lookup_is_some

added theorem AList.toAList_cons

deleted theorem AList.to_alist_cons

Modified Mathlib/Data/List/BigOperators/Basic.lean

added theorem List.alternatingProd_cons'

added theorem List.alternatingProd_cons

added theorem List.alternatingProd_cons_cons'

added theorem List.alternatingProd_cons_cons

added theorem List.alternatingProd_nil

added theorem List.alternatingProd_singleton

deleted theorem List.alternating_prod_cons'

deleted theorem List.alternating_prod_cons

deleted theorem List.alternating_prod_cons_cons'

deleted theorem List.alternating_prod_cons_cons

deleted theorem List.alternating_prod_nil

deleted theorem List.alternating_prod_singleton

Modified Mathlib/Data/List/BigOperators/Lemmas.lean

Modified Mathlib/Data/List/Permutation.lean

added theorem List.permutationsAux2_snd_nil

deleted theorem List.permutations_aux2_snd_nil

Modified Mathlib/Data/List/ProdSigma.lean

Modified Mathlib/Data/List/Rdrop.lean

added theorem List.rdropWhile_idempotent

deleted theorem List.rdrop_while_idempotent

Modified Mathlib/Data/List/Sigma.lean

added theorem List.dlookup_isSome

deleted theorem List.dlookup_is_some

Modified Mathlib/Data/Multiset/Antidiagonal.lean

Modified Mathlib/Data/Multiset/Pi.lean

Modified Mathlib/Data/Multiset/Powerset.lean

Modified Mathlib/Data/Multiset/Sections.lean

Modified Mathlib/Data/Real/CauSeqCompletion.lean

Modified Mathlib/Data/Set/Constructions.lean

deleted theorem FiniteInter.finiteInterClosure_FiniteInter

added theorem FiniteInter.finiteInterClosure_finiteInter

Modified Mathlib/Data/Set/Function.lean

Modified Mathlib/Data/Set/Semiring.lean