leanprover-community/mathlib3

Pull Requests Commits

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

leanprover-community-bot committed 5 years ago

ccd502af

refactor(geometry/manifold): use a sigma type for the total space of the tangent bundle (#3966)

sgouezel committed 5 years ago

7c9a86d4

refactor(field_theory/minimal_polynomial, *): make `aeval`, `is_integral`, and `minimal_polynomial` noncommutative (#4001)

awainverse committed 5 years ago

ecf18c69

doc(slim_check): add suggestion (#4024)

cipher1024 committed 5 years ago

e3057ba4

Slight cleaning up (golfing + shortening line size)

pimsp committed 5 years ago

77027d0d

feat(slim_check): subtype instances for `le` `lt` and `list.perm` (#4027)

cipher1024 committed 5 years ago

a056ccbb

feat(data/padics): universal property of Z_p (#3950)

robertylewis committed 5 years ago

2d40d9c6

ci(scripts/detect_errors.py): enforce silent builds (#4025)

fpvandoorn committed 5 years ago

49173c00

feat(category_theory/filtered): finite diagrams in filtered categories admit cocones (#4026)

kim-em committed 5 years ago

8b277a95

Added module documentation

pimsp committed 5 years ago

13d85dfa

feat(category_theory/limits/concrete): simp lemmas (#3973)

kim-em committed 5 years ago

fa6485a5

feat(geometry/euclidean/circumcenter): more lemmas (#4028)

jsm28 committed 5 years ago

dd633c28

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

leanprover-community-bot committed 5 years ago

c86359f7

fix(docs/100.yaml): fix indentation in 100 list (#4029)

9c02ed19 committed 5 years ago

ca5703d5

fix(test/*): make sure tests produce no output (#3947)

fpvandoorn committed 5 years ago

7b9db99c

feat(order/rel_iso): define `rel_hom` (relation-preserving maps) (#3946)

awainverse committed 5 years ago

9d42f6c6

Finished docstrings of defs and structures

pimsp committed 5 years ago

d1ff7abb

feat(linear_algebra/affine_space): more lemmas (#3990)

jsm28 committed 5 years ago

57463fa4

chore(topology/sheaves): depend less on rfl (#3994)

kim-em committed 5 years ago

71ef45e2

Cleaned up code and started with docstrings

pimsp committed 5 years ago

8d0309a0

chore(algebra/category/CommRing/limits): don't use deprecated.subring (#4010)

kim-em committed 5 years ago

895f6ee7

chore(data/fin): succ_above defn compares fin terms instead of values (#3999)

pechersky committed 5 years ago

ddbdfeb5

feat(ring_theory/localization): Localizations of integral extensions (#3942)

dtumad committed 5 years ago

96c80e24

feat(linear_algebra/eigenspace): add generalized eigenspaces (#4015)

abentkamp committed 5 years ago

cd36773a

feat(field_theory/adjoin): adjoining elements to fields (#3913)

tb65536 committed 5 years ago

7310eab9

feat(ring_theory/localization): localization away from an element (#4019)

101damnations committed 5 years ago

8026ea8a

feat(pfun/recursion): unbounded recursion (#3778)

cipher1024 committed 5 years ago

0b4444ca

doc(slim_check): improve documentation, swap instances (#4023)

cipher1024 committed 5 years ago

d94643c5

feat(slim_check/errors): improve error messages and add useful instances (#4022)

cipher1024 committed 5 years ago

ef22a33f

feat(testing): property based testing (basics) (#3915)

cipher1024 committed 5 years ago

0c2e77c9

Newer Older