leanprover-community/mathlib3

Pull Requests Commits

urkud committed 5 years ago

d6a5b4a7

feat(analysis/normed_space): unconditionally convergent series in `R^n` is absolutely convergent (#4551)

urkud committed 5 years ago

e2dd1c67

refactor(*): migrate to `dense` API (#4447)

urkud committed 5 years ago

2543b688

chore(multiset): dedicated notation for multiset.cons (#4600)

jcommelin committed 5 years ago

fde3d78c

chore(number_theory/arithmetic_function): Define in terms of zero_hom (#4606)

eric-wieser committed 5 years ago

7368d719

feat(analysis/normed_space/operator_norm): construct a continuous_linear_equiv from a linear_equiv and bounds in both directions (#4583)

dupuisf committed 5 years ago

b1c1033f

feat(data/vector2): induction principle, define last, and some lemmas (blocked by #4578) (#4554)

pechersky committed 5 years ago

7cff8250

chore(linear_algebra/finsupp): Implement lsingle in terms of single_add_hom (#4605)

eric-wieser committed 5 years ago

71bb9f23

chore(algebra/monoid_algebra): Replace `algebra_map'` with `single_(zero|one)_ring_hom` (#4582)

eric-wieser committed 5 years ago

ca6af1c4

feat(algebra/char_p): fields with a hom between them have same char (#4594)

jcommelin committed 5 years ago

9f9344d3

feat(data/polynomial/eval): easy lemmas + speedup (#4596)

jcommelin committed 5 years ago

dd8bf2c5

chore(algebra/pointwise): remove `@[simp]` from `singleton_one`/`singleton_zero` (#4592)

urkud committed 5 years ago

7fff35f5

chore(linear_algebra/dimension): more same-universe versions of `is_basis.mk_eq_dim` (#4591)

urkud committed 5 years ago

c9ae9e67

fix(big_operators): fix imports (#4588)

fpvandoorn committed 5 years ago

766d860d

feat(archive/imo): formalize IMO 1962 problem Q1 (#4450)

lacker committed 5 years ago

505b969c

chore(scripts): update nolints.txt (#4587)

leanprover-community-bot committed 5 years ago

e9572699

feat(mv_polynomial): minor simplification in coeff_mul (#4586)

fpvandoorn committed 5 years ago

9eb341a1

feat(archive/imo): formalize IMO 1962 problem 4 (#4518)

lacker committed 5 years ago

7dcaee1c

feat(archive/imo): formalize IMO 1960 problem 1 (#4366)

lacker committed 5 years ago

b231d8e7

feat(data/finsupp): Add `map_finsupp_prod` to homs (#4585)

eric-wieser committed 5 years ago

a6d445db

feat(topology/category/Compactum): Compact Hausdorff spaces (#4555)

adamtopaz committed 5 years ago

d1bb5ea6

feat(data/list/*): add left- and right-biased versions of map₂ and zip (#4512)

JLimperg committed 5 years ago

bc77a23e

chore(algebra/order*): move `abs`/`min`/`max`, review (#4581)

urkud committed 5 years ago

d3d70f1f

feat(tactic/rcases): rcases_many (#4569)

digama0 committed 5 years ago

6ea62008

feta(data/fin): induction principle on fin (n + 1) (#4546)

pechersky committed 5 years ago

9bed4567

chore(control/functor): linting (#4496)

kmill committed 5 years ago

8ccfb0ad

chore(*): update to Lean 3.21.0c (#4578)

bryangingechen committed 5 years ago

9713e960

feat(archive/100-theorems-list/70_perfect_numbers): Direction 1 of the Perfect Number Theorem (#4544)

awainverse committed 5 years ago

6816b835

chore(data/hash_map): linting (#4498)

kmill committed 5 years ago

93790507

fix(algebra/ordered_group): use `add_neg` in autogenerated lemma name (#4580)

urkud committed 5 years ago

266895fb

Older