leanprover-community/mathlib

Pull Requests Commits

chore(category_theory/limits): facts about opposites of limit cones (#4250)

kim-em committed 5 years ago

ff66d924

feat(*): preparations for roots of unity (#4322)

jcommelin committed 5 years ago

da66bb81

feat(algebra/pointwise): Add missing to_additive on finset lemmas (#4306)

eric-wieser committed 5 years ago

743f82ca

feat(data/prod): mk injective lemmas (#4319)

robertylewis committed 5 years ago

669a3499

feat(algebra/invertible): invertible.copy (#4318)

robertylewis committed 5 years ago

d301d431

feat(analysis/special_functions/*): prove that `exp` etc are measurable (#4314)

urkud committed 5 years ago

fa09f493

feat(linear_algebra/dual): transpose of linear maps (#4302)

PatrickMassot committed 5 years ago

744e0675

feat(analysis/normed_space): define `normed_comm_ring` (#4291)

urkud committed 5 years ago

a5a7a753

doc(data/monoid_algebra): fix typo (#4317)

gebner committed 5 years ago

9962bfa7

feat(algebra/quandle): racks and quandles (#4247)

kmill committed 5 years ago

22d034c1

feat(ring_theory/algebra_tower): Artin--Tate lemma (#4282)

kckennylau committed 5 years ago

0bb5e5d9

chore(topology/algebra/ordered): golf a proof (#4311)

urkud committed 5 years ago

88187ba9

refactor(data/nat/basic): review API of `nat.find_greatest` (#4274)

urkud committed 5 years ago

89d8cc37

fix(data/list/basic): Ensure that ball_cons actually works as a simp lemma (#4281)

eric-wieser committed 5 years ago

50dbce94

feat(data/mv_polynomial): some lemmas on constant_coeff and rename (#4231)

jcommelin committed 5 years ago

40fb7017

feat(geometry/euclidean/monge_point): lemmas on altitudes and orthocenter (#4179)

jsm28 committed 5 years ago

8461a7d3

chore(algebra/free_algebra): Make the second type argument to lift and ι implicit (#4299)

eric-wieser committed 5 years ago

7bbb759f

chore(algebra/ordered_ring): remove duplicate lemma (#4295)

kim-em committed 5 years ago

ad680c24

chore(algebra/lie): group Lie algebra files together in their own directory (#4288)

Oliver Nash committed 5 years ago

3986e978

chore(data/fintype/card): review API (#4287)

urkud committed 5 years ago

d77ac51c

feat(data/*/gcd): adds gcd, lcm of finsets and multisets (#4217)

awainverse committed 5 years ago

66c87c0d

chore(category_theory/limits): some limit lemmas (#4238)

b-mehta committed 5 years ago

17618222

feat(ring_theory/integral_closure): Explicitly define integral extensions (#4164)

dtumad committed 5 years ago

d8726bf3

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

leanprover-community-bot committed 5 years ago

2fa1bc62

feat(measure_theory): prove that more functions are measurable (#4266)

fpvandoorn committed 5 years ago

38977584

feat(undergrad.yaml): missing items (#4290)

PatrickMassot committed 5 years ago

c3224710

feat(topology): various additions (#4264)

fpvandoorn committed 5 years ago

2516d7d6

refactor(*): create directory field_theory/finite (#4212)

jcommelin committed 5 years ago

b6ce982d

docs(overview): expand analysis (#4284)

hrmacbeth committed 5 years ago

95ab6ac9

chore(data/option): swap sides in `ne_none_iff_exists` (#4285)

urkud committed 5 years ago

a7e34357

Newer Older