leanprover-community/mathlib3

Pull Requests Commits

perf(tactic/lint/frontend): run linters in parallel (#6293)

gebner committed 5 years ago

96f89335

chore({algebra, algebraic_geometry}/*): move 1 module doc and split lines (#6294)

Julian-Kuelshammer committed 5 years ago

619c1b0d

feat(topology/category/profinite): show Profinite is reflective in CompHaus (#6219)

callesonne committed 5 years ago

5b579a2c

fix(doc/references.bib): fix syntax (#6290)

bryangingechen committed 5 years ago

5a597819

feat(order/pfilter): add preorder filters, dual to preorder ideals (#5928)

mguaypaq committed 5 years ago

2a7eafa5

feat(linear_algebra/dual): adds dual annihilators (#6078)

kex-y committed 5 years ago

017acaee

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

leanprover-community-bot committed 5 years ago

7c267dfa

chore(analysis/normed_space/finite_dimension,topology/metric_space): golf (#6285)

urkud committed 5 years ago

7592a8f4

feat(data/zmod/basic): add simp lemmas about coercions, tidy lemma names (#6280)

eric-wieser committed 5 years ago

bc1c4f24

feat(analysis/normed_space/multilinear): generalized `curry` (#6270)

urkud committed 5 years ago

75f33464

feat(data/fin): pred_above_monotone (#6170)

kim-em committed 5 years ago

152bf15a

doc(tactic/algebra): document @[ancestor] (#6272)

eric-wieser committed 5 years ago

4bae1c47

feat(ring_theory/simple_module): introduce `is_semisimple_module` (#6215)

awainverse committed 5 years ago

07a1b8db

feat(algebra/lie/subalgebra): define lattice structure for Lie subalgebras (#6279)

ocfnash committed 5 years ago

f066eb1a

feat(analysis/normed_space/inner_product): norm is smooth at `x ≠ 0` (#6275)

urkud committed 5 years ago

d43a3bae

feat(data/int/basic): lemmas about int and int.to_nat (#6253)

kim-em committed 5 years ago

b190131f

feat(category/eq_to_hom): lemmas to replace rewriting in objects with eq_to_hom (#6252)

kim-em committed 5 years ago

8b8a5a27

feat(linear_algebra/pi): ext lemma for `f : (Π i, M i) →ₗ[R] N` (#6233)

urkud committed 5 years ago

ea1cff4a

feat(group_theory): prove the 2nd isomorphism theorem for groups (#6187)

AdrianDoM committed 5 years ago

0c61fc46

feat(algebra/ordered_monoid): inequalities involving mul/add (#6171)

benjamindavidson committed 5 years ago

9b3008eb

feat(ring_theory/ideal/operations) : add lemma prod_eq_bot (#5795)

faenuccio committed 5 years ago

3c157512

chore(topology/sheaves): speed up slow proofs by tidy (#6274)

kim-em committed 5 years ago

11f054bb

feat(data/fin): refactor `pred_above` (#6125)

kim-em committed 5 years ago

5258de08

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

leanprover-community-bot committed 5 years ago

b2dbfd6f

feat(topology/category/Top): nonempty inverse limit of compact Hausdorff spaces (#6271)

kmill committed 5 years ago

d4ef2e85

feat(data/set/finite): complement of finite set is infinite (#6266)

kbuzzard committed 5 years ago

bf9ca8b5

feat(option/basic): add join_eq_none (#6269)

fpvandoorn committed 5 years ago

7a7a5591

feat(data/real/liouville, ring_theory/algebraic): a Liouville number is transcendental! (#6204)

adomani committed 5 years ago

781cc63f

feat(algebra/category/Module): the free/forgetful adjunction for R-modules (#6168)

kim-em committed 5 years ago

efa6877b

feat(algebra/algebra,linear_algebra): add *_equiv.of_left_inverse (#6167)

eric-wieser committed 5 years ago

3bf72416

Newer Older