leanprover-community/mathlib3

Pull Requests Commits

fix(algebra/archimedean): swap names of floor_add_fract and fract_add_floor (#770)

ChrisHughes24 committed 6 years ago

Verified 05d1d339

feat(linarith): improve handling of strict inequalities in nat and int (#769)

kim-em committed 6 years ago

42d1ed70

fix(docs/howto-contribute): main repository has moved

PatrickMassot committed 6 years ago

Verified 3f477395

fix(scripts/update_mathlib): improve python style and error handling (#759)

PatrickMassot committed 6 years ago

7450cc55

fix(scripts/update-mathlib): cached archived were never expanded

cipher1024 committed 6 years ago

Verified 71a7e1c4

fix(scripts/update-mathlib): fix the commit check

cipher1024 committed 6 years ago

Verified 42224838

doc(nat/decidable_prime): add docstrings explaining the two decidable_prime instances (#757)

kim-em committed 6 years ago

e23553a4

feat(ring_theory/polynomial): more operations on polynomials (#679)

kckennylau committed 6 years ago

f9220866

chore(linear_algebra/multivariate_polynomial): remove unnecessary decidable_eq assumption (#755)

kckennylau committed 6 years ago

c9b2d0ee

feat(*): polar co-ordinates, de moivre, trig identities, quotient group for angles (#745)

abhimanyupallavisudhir committed 6 years ago

ddc016c6

fix(analysis/specific_limits): remove useless assumption (#751)

sgouezel committed 6 years ago

63fa61db

feat(order_dual): instances for order_dual and shortening proofs (#746)

ChrisHughes24 committed 6 years ago

Verified e739cf50

feat(field_theory/subfield): closure of subset in field (#742)

kckennylau committed 6 years ago

3c3a0521

feat(data/finmap): lift_on₂ (#716)

spl committed 6 years ago

96564857

fix(order/basic): give order_dual the correct lt (#741)

ChrisHughes24 committed 6 years ago

Verified 8b8ae32c

feat(analysis/exponential): pow_nat_rpow_nat_inv (#740)

ChrisHughes24 committed 6 years ago

Verified c7202e57

feat(data/fintype): fintype.of_injective

ChrisHughes24 committed 6 years ago

78ce6e49

feat(data/alist,data/finmap): always insert key-value pair (#722)

spl committed 6 years ago

9a2c13ab

feat(data/polynomial): create nonzero_comm_semiring and generalize nonzero_comm_ring lemmas (#736)

ChrisHughes24 committed 6 years ago

Verified 6b4435be

feat(ring_theory/localization): revamp, ideal embedding (#481)

kckennylau committed 6 years ago

c64b67ed

feat(category/monad/cont): continuation passing monad (#728)

cipher1024 committed 6 years ago

Verified 17f9bef0

refactor(data/equiv/algebra): move polynomial lemmas from equiv/algebra to mv_polynomial (#731)

ChrisHughes24 committed 6 years ago

Verified 0a6e7057

chore(order/filter/basic): update documentation of filter_upwards

kckennylau committed 6 years ago

d80b03e6

chore(topology/algebra/topological_structures): remove unused import (#729)

ChrisHughes24 committed 6 years ago

Verified 8730619b

refactor(data/equiv): rename subtype_equiv_of_subtype to subtype_congr and subtype_congr to subtype_congr_prop

johoelzl committed 6 years ago

ce580d7b

feat(data/equiv/basic): generalise subtype_equiv_of_subtype (#724)

jcommelin committed 6 years ago

683519f3

fix(data/subtype): don't use pattern matching in subtype.map (#725)

rwbarton committed 6 years ago

d4568a41

chore(deploy): clean up deploy_nightly.sh (#720)

rwbarton committed 6 years ago

5da8605f

refactor(data/real): move cau_seq_filter to analysis/metric_space (#723)

sgouezel committed 6 years ago

a6150a32

refactor(topology/algebra/infinite_sum): Cauchy condition for infinite sums generalized to complete topological groups

johoelzl committed 6 years ago

3fd0e60a

Newer Older