leanprover-community/mathlib

Pull Requests Commits

Merge branch 'digits_prefix' of https://github.com/leanprover-community/mathlib into digits_prefix

Pazzaz committed 4 years ago

09a8a09e

Pazzaz committed 4 years ago

02b0d234

Pazzaz committed 4 years ago

Verified 70d5a9ee

Remove a hypothesis from`digits_of_digits_prefix`

Pazzaz committed 4 years ago

7e644e54

Remove unnecessary lemmas

Pazzaz committed 4 years ago

0ec0b501

Add docs for `digits_of_digits_prefix`

Pazzaz committed 4 years ago

7ef8d837

Add various lemmas about digits

Pazzaz committed 4 years ago

17e3c55a

chore(scripts): update nolints.txt (#7810)

leanprover-community-bot committed 4 years ago

b806fd43

chore(topology/bases): Rename + unprotect some lemmas (#7809)

adamtopaz committed 4 years ago

36decf5a

chore(data/padics): move padics to number_theory/ (#7771)

kim-em committed 4 years ago

8422d8c7

feat(order/filter/archimedean): in an archimedean linear ordered ring, `at_top` and `at_bot` are countably generated (#7751)

ADedecker committed 4 years ago

adae1adf

refactor(linear_algebra/finsupp): replace mem_span_iff_total (#7735)

kim-em committed 4 years ago

6d85ff23

feat(analysis/fourier): monomials on the circle are orthonormal (#6952)

hrmacbeth committed 4 years ago

6d90d35f

chore(data/*/gcd): move data/*set/gcd to algebra/gcd_monoid/ (#7800)

kim-em committed 4 years ago

4b312472

chore(data/zsqrtd): move to number_theory/ (#7796)

kim-em committed 4 years ago

e5915436

chore(data/fincard): move to set_theory/ (#7795)

kim-em committed 4 years ago

ce3ca596

chore(data/hash_map): remove duplicate imports (#7794)

kim-em committed 4 years ago

d5a635be

chore(data/quaternion): move to algebra/ (#7793)

kim-em committed 4 years ago

a36560c2

chore(data/equiv): add docstrings (#7704)

YaelDillies committed 4 years ago

7e3e8834

feat(tactic/lint): add linter that type-checks statements (#7694)

fpvandoorn committed 4 years ago

29d0a4e6

feat(measure_theory/integration): add a version of the monotone convergence theorem using `tendsto` (#7791)

ADedecker committed 4 years ago

6e5899dd

chore(logic/small): reduce imports (#7777)

kim-em committed 4 years ago

82bc3ca6

chore(data/support): move data/(support|indicator_function) to algebra/ (#7774)

kim-em committed 4 years ago

47dbdaca

feat(algebra/algebra/subalgebra): add subalgebra.prod (#7782)

riccardobrasca committed 4 years ago

173bc4c2

doc(data/finsupp/pointwise): update old module doc (#7770)

kim-em committed 4 years ago

b231c923

refactor(data/nnreal): rename nnreal.of_real to real.to_nnreal (#7750)

sgouezel committed 4 years ago

b91cdb91

chore(scripts): update nolints.txt (#7798)

leanprover-community-bot committed 4 years ago

832aff84

feat(topology/sheaves/stalks): Small lemmas about stalk pushforward and stalk map (#7789)

justus-springer committed 4 years ago

cdf6cf0f

refactor(algebraic_geometry/structure_sheaf): Rename Spec.Top to prime_spectrum.Top (#7786)

justus-springer committed 4 years ago

21641075

chore(order/omega_complete_partial_order): clean up references (#7781)

YaelDillies committed 4 years ago

2fd0ff48

Older