leanprover-community/mathlib3

Pull Requests Commits

awainverse committed 3 years ago

019b3e2e

awainverse committed 3 years ago

9f26b867

awainverse committed 3 years ago

03fa68f1

awainverse committed 3 years ago

5082d1be

awainverse committed 3 years ago

e48e9b5d

awainverse committed 3 years ago

3167c2a9

Merge remote-tracking branch 'origin/master' into formula_simp

awainverse committed 3 years ago

5c020eb8

Revert "no_rel"

awainverse committed 3 years ago

2b75186e

chore(topology/bases): golf a proof (#12127)

urkud committed 3 years ago

518b5d25

awainverse committed 3 years ago

4cf3cf9e

awainverse committed 3 years ago

3000a365

Revert "revert"

awainverse committed 3 years ago

5fe58a91

awainverse committed 3 years ago

619362ab

feat(algebra/group/pi): add pi.nsmul_apply (#12122)

alexjbest committed 3 years ago

213e2ed7

feat(tactic/swap_var): name juggling, a weaker wlog (#12006)

pechersky committed 3 years ago

b3d09448

fix(category_theory/limits): improve inaccurate docstrings (#12130)

TwoFX committed 3 years ago

5f46dd09

feat(number_theory/divisors): add `prod_div_divisors` and `sum_div_divisors` (#12087)

stuart-presnell committed 3 years ago

7b6c4072

refactor(topology/metric_space/completion): change namespace (#12077)

urkud committed 3 years ago

33179f7e

feat(data/nat/fib): add that `fib` is sum of `nat.choose` along antidiagonal (#12063)

kmill committed 3 years ago

18c3e3f0

refactor(group_theory/abelianization): Define `commutator` in terms of `general_commutator` (#11949)

tb65536 committed 3 years ago

ffc2bdfb

refactor(ring_theory/fractional_ideal): rename lemmas for dot notation, add coe_pow (#12080)

eric-wieser committed 3 years ago

018c7289

feat(ring_theory/fractional_ideal): add coe_ideal lemmas (#12073)

mariainesdff committed 3 years ago

bcf8a6ed

awainverse committed 3 years ago

49428203

feat(algebra/big_operators/intervals): summation by parts (#11814)

ecstatic-morse committed 3 years ago

98643bca

feat(data/equiv): define `ring_equiv_class` (#11977)

Vierkantor committed 3 years ago

3ca16d0a

chore(algebra/star/self_adjoint): extract a lemma from `has_scalar` (#12121)

eric-wieser committed 3 years ago

223f1496

doc(analysis/normed/group/basic): add docstring explaining the "insert" name (#12100)

eric-wieser committed 3 years ago

aed97e03

fix(category_theory/limits/shapes/images): make class a Prop (#12119)

jcommelin committed 3 years ago

3e6439cd

refactor(topology/algebra): reorder imports (#12089)

urkud committed 3 years ago

33b4e739

feat(data/finset/basic): add lemma `filter_eq_empty_iff` (#12104)

stuart-presnell committed 3 years ago

77f264f1

Older