leanprover-community/mathlib

Pull Requests Commits

Removed cyclic import

foxthomson committed 4 years ago

f62912da

Update default.lean

foxthomson committed 4 years ago

2c4f783e

Move to new file and cleanup

foxthomson committed 4 years ago

636dd664

Added elab_as_eliminator

foxthomson committed 4 years ago

4eb87881

foxthomson committed 4 years ago

b4109af3

feat(algebra/lie/basic): Lie ideal operations are linear spans (#5676)

Oliver Nash committed 5 years ago

f60c184e

feat(measure_theory/lp_space): add more lemmas about snorm (#5644)

RemyDegenne committed 5 years ago

5faf34cc

chore(data/set/lattice): add a few simp lemmas (#5671)

urkud committed 5 years ago

fdec90ad

feat(topology/separation, topology/metric_space/basic): add lemmas on discrete subsets of a topological space (#5523)

adomani committed 5 years ago

3166f4ef

feat(topology/algebra/ordered): prove `tendsto.Icc` for pi-types (#5639)

urkud committed 5 years ago

a161256c

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

leanprover-community-bot committed 5 years ago

faf1a983

feat(category_theory/limits): preserving pullbacks (#5668)

b-mehta committed 5 years ago

12945004

chore(linear_algebra/alternating): golf a proof (#5666)

eric-wieser committed 5 years ago

ce34ae6a

chore(algebra/group/hom): fix additive version of docstring (#5660)

jcommelin committed 5 years ago

0cd70d09

chore(analysis/special_functions/trigonometric): adding `@[pp_nodot]` to complex.log (#5670)

JamesAMaths committed 5 years ago

2b5344f5

feat(data/finset/intervals, data/set/intervals/basic): intersection of finset.Ico, union of intervals for sets and finsets (#5410)

RemyDegenne committed 5 years ago

aab5994e

feat(algebra/linear_ordered_comm_group_with_zero): Add linear_ordered_comm_monoid_with_zero and an instance for nat (#5645)

eric-wieser committed 5 years ago

d935760d

feat(geometry/manifold/times_cont_mdiff): API for checking `times_cont_mdiff` (#5631)

hrmacbeth committed 5 years ago

2bde21d1

feat(category_theory/closed): Frobenius reciprocity of cartesian closed categories (#5624)

b-mehta committed 5 years ago

bd9b03f6

feat(measure_theory/measure_space): ae_measurable and measurable are equivalent for complete measures (#5643)

RemyDegenne committed 5 years ago

0d7ca986

refactor(linear_algebra/alternating): Use unapplied maps when possible (#5648)

eric-wieser committed 5 years ago

9f066f1f

chore(algebra/ordered_monoid): rename lemmas (#5657)

fpvandoorn committed 5 years ago

795d5ab6

feat(measure_theory/borel_space): locally finite measure is sigma finite (#5634)

urkud committed 5 years ago

611bc865

refactor(algebra/module/basic): Clean up all the nat/int semimodule definitions (#5654)

eric-wieser committed 5 years ago

efdcab1a

feat(topology/algebra): add additive/multiplicative instances (#5662)

fpvandoorn committed 5 years ago

d89464d2

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

leanprover-community-bot committed 5 years ago

7500b242

feat(measure_theory): some additions (#5653)

fpvandoorn committed 5 years ago

4c3c8d78

chore(data/list/basic): tag mmap(') with simp (#5443)

pechersky committed 5 years ago

33a86cff

feat(category_theory/sites): category of sheaves on the trivial topology (#5651)

b-mehta committed 5 years ago

18ba69b7

feat(category_theory/monad): reflector preserves terminal object (#5649)

b-mehta committed 5 years ago

3c5d5c51

Older