leanprover-community/mathlib

Pull Requests Commits

cleanup(category_theory/cones): tidying up, after making opposites work better (#675)

kim-em committed 6 years ago

a09dc9f2

fix(category_theory/equivalence): duplicated namespace prefix (#669)

kim-em committed 6 years ago

b084cfcd

fix(replacer): better flow control in replacer when tactic fails (#673)

kim-em committed 6 years ago

e501d026

feat(ring_theory/algebra): subalgebra_of_subring (#664)

kckennylau committed 6 years ago

0393ccbd

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

kim-em committed 6 years ago

f529870e

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

kckennylau committed 6 years ago

6925e4dc

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

kim-em committed 6 years ago

fb601459

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

kckennylau committed 6 years ago

ed0d24af

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

minchaowu committed 6 years ago

d8f6dc46

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

minchaowu committed 6 years ago

a32de36f

add printing for conclusions of sintros

minchaowu committed 6 years ago

a08c9a72

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

robertylewis committed 6 years ago

c9e4f8ed

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

robertylewis committed 6 years ago

52adfd73

feat(ring_theory/noetherian): is_noetherian_ring_range

kckennylau committed 6 years ago

89bc63c3

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

kckennylau committed 6 years ago

8e381f6e

chore(test): fix test directory structure

cipher1024 committed 6 years ago

50a03f76

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

rwbarton committed 6 years ago

12be0aaa

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

rwbarton committed 6 years ago

829b49bd

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

johoelzl committed 6 years ago

0eb9db6a

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

ChrisHughes24 committed 6 years ago

a480160a

feat(group_theory): monoid / group closure of union

kckennylau committed 6 years ago

065f083b

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

johoelzl committed 6 years ago

f7b9d6b4

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

ChrisHughes24 committed 6 years ago

aa944bff

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

sgouezel committed 6 years ago

626489ad

second countability criteria in metric spaces

sgouezel committed 6 years ago

ef35c6c3

cleanup instances/ennreal

sgouezel committed 6 years ago

30649f55

feat(ring_theory/polynomial): hilbert basis theorem

kckennylau committed 6 years ago

afa535e7

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

johoelzl committed 6 years ago

860eba67

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

johoelzl committed 6 years ago

247dcb2d

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

cipher1024 committed 6 years ago

4fb6c7dc

Newer Older