leanprover-community/mathlib3

Pull Requests Commits

chore(*): Use `multilinear_map.mk_pi_algebra_fin` in place of a manual definition, and fix resulting errors

eric-wieser committed 5 years ago

d550c3d0

Merge branch 'master' of github.com:leanprover-community/mathlib into exterior_algebra

eric-wieser committed 5 years ago

3439d7de

feat(data/complex/module): ![1, I] is a basis of C over R (#4713)

urkud committed 5 years ago

8489972a

chore(*): review some lemmas about injectivity of coercions (#4711)

urkud committed 5 years ago

cf551ee3

chore(.gitignore): gitignore for emacs temp files (#4699)

lacker committed 5 years ago

5d52ea42

fix(tactic/norm_num): remove one_div from simp set (#4705)

digama0 committed 5 years ago

8131349c

feat(linear_algebra/affine_space/ordered): define `slope` (#4669)

urkud committed 5 years ago

617e8295

chore(data/finsupp): minor review (#4712)

urkud committed 5 years ago

b46190f9

chore(data/polynomial): slightly generalize `map_eq_zero` and `map_ne_zero` (#4708)

urkud committed 5 years ago

288802b6

chore(topology/algebra/ordered): drop section vars, golf 2 proofs (#4706)

urkud committed 5 years ago

21415c8c

chore(data/set): a few more lemmas about `image2` (#4695)

urkud committed 5 years ago

0cf8a98b

feat(data/real/pi): Leibniz's series for pi (#4228)

hrmacbeth committed 5 years ago

050b5a1b

feat(measure_theory): finite_spanning_sets_in (#4668)

fpvandoorn committed 5 years ago

cd884eb8

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

leanprover-community-bot committed 5 years ago

9755ae3c

chore(data/finsupp): `to_additive` on `on_finset_sum` (#4698)

urkud committed 5 years ago

accc50ed

chore(data/multiset): add a few lemmas (#4697)

urkud committed 5 years ago

706b4841

refactor(ring_theory/witt_vector): move lemmas to separate file (#4693)

jcommelin committed 5 years ago

b707e989

feat(algebra/free_algebra): Add a ring instance (#4692)

eric-wieser committed 5 years ago

b3003023

doc(algebra/algebra/basic): Fixes some documentation about `R`-algebras (#4689)

adamtopaz committed 5 years ago

cc6594a5

chore(topology/instances/ennreal): prove `nnreal.not_summable_iff_tendsto_nat_at_top` (#4670)

urkud committed 5 years ago

86d65f8d

feat({field,ring}_theory/adjoin): generalize `induction_on_adjoin` (#4647)

Vierkantor committed 5 years ago

30195815

feat(data/polynomial/reverse): define `reverse f`, prove that `reverse` is a multiplicative monoid homomorphism (#4598)

adomani committed 5 years ago

006b2e70

feat(tactic/unify_equations): add unify_equations tactic (#4515)

JLimperg committed 5 years ago

0c70cf30

feat(archive/imo): formalize IMO 1998 problem 2 (#4502)

Oliver Nash committed 5 years ago

a249c9a4

feat(data/monoid_algebra): add missing has_coe_to_fun (#4315)

eric-wieser committed 5 years ago

5065471e

chore(logic/function): `simp`lify applications of `(un)curry` (#4696)

urkud committed 5 years ago

0523b61d

Revert "chore(data/multiset): add a few lemmas"

urkud committed 5 years ago

a1f17706

chore(data/multiset): add a few lemmas

urkud committed 5 years ago

45caa4f3

fix(tactic/norm_num): remove unnecessary argument to rat.cast_zero (#4682)

bryangingechen committed 5 years ago

cacc297c

feat(ring_theory/witt_vector/structure_polynomial): examples and basic properties (#4467)

jcommelin committed 5 years ago

0f1bc68f

Older