leanprover-community/mathlib3

Pull Requests Commits

refactor(data/mv_polynomial): move `smul` lemmas into basic.lean (#4097)

shingtaklam1324 committed 5 years ago

d5be9f38

feat(data/mv_polynomial): a few facts about `constant_coeff` and `aeval` (#4085)

robertylewis committed 5 years ago

19b9ae6e

feat(slim_check): make `shrink` recursive (#4038)

cipher1024 committed 5 years ago

d857def3

feat(data/{int,nat}/cast): dvd cast lemmas (#4086)

robertylewis committed 5 years ago

55cab6c0

feat(ring_theory/dedekind_domain): definitions (#4000)

knaka3435 committed 5 years ago

49bb92dc

feat(linear_algebra): add `restrict` for endomorphisms (#4053)

abentkamp committed 5 years ago

8e9b1f0f

feat(linear_algebra): tiny missing pieces (#4089)

PatrickMassot committed 5 years ago

47264da1

feat(data/polynomial/ring_division): make `polynomial.roots` a multiset (#4061)

Vierkantor committed 5 years ago

9f55ed70

feat(topology): misc topological lemmas (#4091)

PatrickMassot committed 5 years ago

660a6c49

feat(ordered_field): missing inequality lemmas (#4090)

PatrickMassot committed 5 years ago

9da39cf9

doc(*): add some docstrings (#4073)

kbuzzard committed 5 years ago

0967f841

feat(tactic/explode): correctly indent long statements (#4084)

gebner committed 5 years ago

44d356c4

fix(data/mv_polynomial/pderivative): rename variables and file, make it universe polymorphic (#4083)

shingtaklam1324 committed 5 years ago

11e62b0b

fix(tactic/linarith): treat powers like multiplication (#4082)

robertylewis committed 5 years ago

98061d12

doc(ring_theory/localization): fix docstring typo (#4081)

rwbarton committed 5 years ago

d6e7ee07

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

jsm28 committed 5 years ago

297a14e4

feat(order/conditionally_complete_lattice, topology/algebra/ordered): inherited order properties for `ord_connected` subset (#3991)

hrmacbeth committed 5 years ago

40de35aa

chore(*): use new `extends_priority` default of 100 (#4066)

rwbarton committed 5 years ago

2ab31f91

refactor(data/mv_polynomial): split into multiple files (#4070)

robertylewis committed 5 years ago

77c8415b

feat(data/equiv/basic): add ext_iff for perm (#4067)

chrispvm committed 5 years ago

d5580f44

feat(analysis/special_functions/pow): Added lemmas bounding rpow in ennreal (#4039)

benjamindavidson committed 5 years ago

f5ee84c9

fix(topology/metric_space): free universe (#4072)

PatrickMassot committed 5 years ago

73540423

doc(*): add docstrings (#4071)

kbuzzard committed 5 years ago

dde8bad7

chore(data/padics): fix bad markdown in doc string (#4068)

robertylewis committed 5 years ago

b2ec2b0c

feat(geometry/euclidean/basic): reflection lemmas (#4056)

jsm28 committed 5 years ago

4f1399de

feat(function): has_uncurry (#3694)

PatrickMassot committed 5 years ago

445e883e

doc(tactic/lean_core_docs): congr understands subsingletons (#4060)

lambda-fairy committed 5 years ago

1c53f912

doc(algebra/group/to_additive): order of to_additive relative to other attributes (#4065)

rwbarton committed 5 years ago

a16112d3

feat(ring_theory/unique_factorization_domain): descending chain condition for divisibility (#4031)

awainverse committed 5 years ago

c7d6a8e7

feat(category_theory): colimits for pi categories (#4054)

cipher1024 committed 5 years ago

851e83ec

Older