leanprover-community/mathlib3

Pull Requests Commits

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

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

kmill committed 4 years ago

d4ef2e85

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

kbuzzard committed 4 years ago

bf9ca8b5

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

fpvandoorn committed 4 years ago

7a7a5591

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

adomani committed 4 years ago

781cc63f

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

kim-em committed 4 years ago

efa6877b

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

eric-wieser committed 4 years ago

3bf72416

chore(topology/basic): add `continuous_at_congr` and `continuous_at.congr` (#6267)

urkud committed 4 years ago

2289b185

doc(*): remove `\\` hack for latex backslashes in markdown (#6263)

robertylewis committed 4 years ago

0b4823cc

doc(algebraic_geometry/structure_sheaf): fix latex (#6262)

robertylewis committed 4 years ago

16eb4af7

feat(analysis/special_functions): strict differentiability of `real.exp` and `real.log` (#6256)

urkud committed 4 years ago

7459c21c

feat(analysis/special_functions): `sqrt` is infinitely smooth at `x ≠ 0` (#6255)

urkud committed 4 years ago

b0071f3f

Newer Older