leanprover-community/mathlib3

Pull Requests Commits

feat(analysis/special_functions/trigonometric): Added lemmas for deriv of tan (#3746)

benjamindavidson committed 5 years ago

fabf34f4

feat(data/mv_polynomial): fill in API for vars (#4018)

robertylewis committed 5 years ago

62963861

chore(data/finset/lattice): remove unneeded assumptions (#4020)

jcommelin committed 5 years ago

7b3c653b

feat(computability/encoding): define encoding of basic data types (#3976)

MadPidgeon committed 5 years ago

815a2f97

feat(linear_algebra/char_poly): rephrase Cayley-Hamilton with `aeval', define `matrix.min_poly` (#4040)

awainverse committed 5 years ago

364d5d4c

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

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

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)

Qian Hong 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

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

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

Newer Older