leanprover-community/mathlib

Pull Requests Commits

rename finset_sum_divisors_iff to finset_sum_divisors

nielsvoss committed 2 years ago

b5ce7d56

clean up finset.sum_bij call in finset_sum_divisors_iff

nielsvoss committed 2 years ago

54829571

remove some extra lemmas

nielsvoss committed 2 years ago

d1d9afc4

prove finset_sum_divisors_iff

nielsvoss committed 2 years ago

3eedad4c

add finset_sum_divisors_iff' lemma

nielsvoss committed 2 years ago

efc8aa69

start work on multiplicative_of_mul_multiplicative

nielsvoss committed 2 years ago

680b65be

start working on dirichlet_inv_multiplicative

nielsvoss committed 2 years ago

575576cf

add is_dirichlet_inv_eq_dirichlet_inv lemma

nielsvoss committed 2 years ago

444b4196

use lemma keyword more often and do general cleanup

nielsvoss committed 2 years ago

4a3ae676

add lemmas about canceling multiplication

nielsvoss committed 2 years ago

11b42452

remove set k statement from proof of dirichlet_inv_is_inv

nielsvoss committed 2 years ago

d90f70da

simplify proof of dirichlet_inv_is_inv

nielsvoss committed 2 years ago

a13086e5

finish proof of dirichlet_inv_is_inv

nielsvoss committed 2 years ago

9c98e1c1

do more work on dirichlet_inv_is_inv

nielsvoss committed 2 years ago

f52d6026

create helper lemmas for dirichlet_inv_is_inv

nielsvoss committed 2 years ago

4272ffc8

complete n = 0 and n = 1 cases of dirichlet_inv_is_inv

nielsvoss committed 2 years ago

dc8035f9

prove that dirichlet_inv_fun terminates

nielsvoss committed 2 years ago

088fcb0d

remove sorry in dirichlet_inv_to_fun

nielsvoss committed 2 years ago

dfdea866

add lemmas about recursive case of dirichlet_inv_fun

nielsvoss committed 2 years ago

1c927ddf

start working on defining a function to get the dirichlet inverse

nielsvoss committed 2 years ago

53ac4165

rename dirichlet_inverse.lean to dirichlet_inv.lean

nielsvoss committed 2 years ago

71762bcc

start work on dirichlet inverses

nielsvoss committed 2 years ago

2ca0cd71

chore(field_theory/minpoly): Split results from `minpoly.lean` into three files (#18048)

Paul-Lez committed 2 years ago

d3e8e0a0

chore(data/fin/basic): Remove elab_strategy (#18049)

PatrickMassot committed 2 years ago

3387923e

feat(topology/algebra/module/multilinear): add continuous versions of constructions (#18044)

eric-wieser committed 2 years ago

44b58b42

feat(analysis/bounded_variation): remove [nonempty] from comp_anti/mono lemmas + golf (#18037)

alreadydone committed 2 years ago

ce967b52

feat(category_theory/mittag_leffler): Introduce the Mittag-Leffler condition (#17905)

bottine committed 2 years ago

6cb77a8e

chore(algebra/big_operators/basic): generalize `finset.prod_of_empty` (#18045)

eric-wieser committed 2 years ago

ab3a26d5

chore(*): add mathlib4 synchronization comments (#17979)

leanprover-community-bot committed 2 years ago

c3291da4

chore(analysis/inner_product_space/basic): golf proofs (#18043)

Ruben-VandeVelde committed 2 years ago

2258b40d

Older