leanprover-community/mathlib3

Pull Requests Commits

half finished decimal expansions

kbuzzard committed 7 years ago

65a75b02

feat(data/nat/gcd/coprime): some easy simp lemmas (#677)

kim-em committed 7 years ago

f529870e

feat(algebra/euclidean_domain): lcm (#665)

kckennylau committed 7 years ago

6925e4dc

cleanup: replace `begin intros ...` with lambdas (#672)

kim-em committed 7 years ago

fb601459

feat(algebra/euclidean_domain): add quotient_zero axiom to euclidean_domain (#666)

kckennylau committed 7 years ago

ed0d24af

feat(src/tactic/explode): improve printing of references

minchaowu committed 7 years ago

d8f6dc46

feat(src/tactic/explode): add printing for conclusions of sintros

minchaowu committed 7 years ago

a32de36f

add printing for conclusions of sintros

minchaowu committed 7 years ago

a08c9a72

fix(tactic/inarith): fix denominator normalization of products

robertylewis committed 7 years ago

c9e4f8ed

feat(tactic,tactic/interactive): add set tactic, a variant of let

robertylewis committed 7 years ago

52adfd73

feat(ring_theory/noetherian): is_noetherian_ring_range

kckennylau committed 7 years ago

89bc63c3

feat(ring_theory/algebra_operations): multiplication of submodules of an algebra (#658)

kckennylau committed 7 years ago

8e381f6e

chore(test): fix test directory structure

cipher1024 committed 7 years ago

50a03f76

refactor(category_theory/instances): rename `examples` to `instances`

rwbarton committed 7 years ago

12be0aaa

chore(.travis.yml): use git clean to clean out untracked files (#659)

rwbarton committed 7 years ago

829b49bd

chore(linear_algebra/multivariate_polynomial): move rename to the right place

johoelzl committed 7 years ago

0eb9db6a

feat(data/polynomial): generalize theorems from nonzero_comm_ring to comm_ring (#653)

ChrisHughes24 committed 7 years ago

a480160a

feat(group_theory): monoid / group closure of union

kckennylau committed 7 years ago

065f083b

refactor(data/equiv/algebra): mv_polynomial mv_polynomial (β ⊕ γ) α ≃r mv_polynomial β (mv_polynomial γ α)

johoelzl committed 7 years ago

f7b9d6b4

feat(analysis/exponential): real powers, `cpow_nat_inv_pow` (#647)

ChrisHughes24 committed 7 years ago

aa944bff

feat(topology/metric_space): diameter of a set in metric spaces (#651)

sgouezel committed 7 years ago

626489ad

second countability criteria in metric spaces

sgouezel committed 7 years ago

ef35c6c3

cleanup instances/ennreal

sgouezel committed 7 years ago

30649f55

feat(ring_theory/polynomial): hilbert basis theorem

kckennylau committed 7 years ago

afa535e7

chore(.): change occurrences of tests directory to test

johoelzl committed 7 years ago

860eba67

feat(linear_algebra): rules for kernel of `of_le`, `cod_restrict`, and `pair`

johoelzl committed 7 years ago

247dcb2d

chore(test): rename the test directory so that `leanpkg` will find it

cipher1024 committed 7 years ago

4fb6c7dc

feat(data/complex/basic): of_real_fpow (#640)

ChrisHughes24 committed 7 years ago

fc529b6f

docs(tactic/monotonicity/interactive): fix `mono` documentation [ci-skip]

rwbarton committed 7 years ago

d7d90fa6

rwbarton committed 7 years ago

0924ac0e

Older