leanprover-community/mathlib3

Pull Requests Commits

fpvandoorn committed 4 years ago

acd42141

fpvandoorn committed 4 years ago

f3c8b2f5

fpvandoorn committed 4 years ago

752e83b0

fpvandoorn committed 4 years ago

1be7705e

fpvandoorn committed 4 years ago

7fa8ab6d

fpvandoorn committed 4 years ago

fd638c97

first try on integrating away certain variables

fpvandoorn committed 4 years ago

3285265e

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

Julian-Kuelshammer committed 4 years ago

619c1b0d

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

callesonne committed 4 years ago

5b579a2c

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

bryangingechen committed 4 years ago

5a597819

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

mguaypaq committed 4 years ago

2a7eafa5

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

kex-y committed 4 years ago

017acaee

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

leanprover-community-bot committed 4 years ago

7c267dfa

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

urkud committed 4 years ago

7592a8f4

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

eric-wieser committed 4 years ago

bc1c4f24

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

urkud committed 4 years ago

75f33464

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

kim-em committed 4 years ago

152bf15a

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

eric-wieser committed 4 years ago

4bae1c47

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

awainverse committed 4 years ago

07a1b8db

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

ocfnash committed 4 years ago

f066eb1a

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

urkud committed 4 years ago

d43a3bae

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

kim-em committed 4 years ago

b190131f

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

kim-em committed 4 years ago

8b8a5a27

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

urkud committed 4 years ago

ea1cff4a

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

AdrianDoM committed 4 years ago

0c61fc46

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

benjamindavidson committed 4 years ago

9b3008eb

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

faenuccio committed 4 years ago

3c157512

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

kim-em committed 4 years ago

11f054bb

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

kim-em committed 4 years ago

5258de08

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

leanprover-community-bot committed 4 years ago

b2dbfd6f

Older