leanprover-community/mathlib

Pull Requests Commits

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

feat(algebra/*_power): simplify `(-a)^(bit0 _)` and `(-a)^(bit1 _)` (#4573)

urkud committed 5 years ago

b3ce8837

feat(archive/imo): IMO 2020 Q2 (#4565)

jsm28 committed 5 years ago

38e9ed32

feat(algebra/free_algebra): Add an inductive principle (#4335)

eric-wieser committed 5 years ago

5022425a

feat(analysis/normed_space/multilinear): define `mk_pi_algebra` (#4316)

urkud committed 5 years ago

3d1f16aa

refactor(field_theory): Adjoin intermediate field (#4468)

tb65536 committed 5 years ago

1362701b

feat(data/polynomial/degree/erase_lead): definition and basic lemmas (#4527)

adomani committed 5 years ago

8fa91251

feat(ring_theory/witt_vector/structure_polynomial): witt_structure_int_prop (#4466)

jcommelin committed 5 years ago

0bfc68fc

feat(set_theory/cardinal): cardinality of powerset (#4576)

b-mehta committed 5 years ago

b9537177

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

leanprover-community-bot committed 5 years ago

81b8123d

chore(topology/algebra/group): review (#4570)

urkud committed 5 years ago

665cc13c

Newer Older