leanprover-community/mathlib3

Pull Requests Commits

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

chore(logic/embedding): move some algebra content (#7776)

kim-em committed 4 years ago

5a42f808

feat(topology/bases): Topological basis of a product. (#7753)

adamtopaz committed 4 years ago

6c912dec

feat(order/[conditionally_]complete_lattice): add more intro lemmas for [c][Sup, Inf] and [c][supr, infi] (#7730)

ADedecker committed 4 years ago

4884ea53

feat(data/finset/noncomm_prod): finset products over monoid (#7567)

pechersky committed 4 years ago

6b2c7a75

feat(ring_theory/adjoin/basic): add missing lemmas (#7780)

riccardobrasca committed 4 years ago

681b9c29

chore(data/nat): split out data/nat/pow (#7758)

kim-em committed 4 years ago

76f41e7e

feat(category_theory/abelian): abelian categories with enough projectives have projective resolutions (#7488)

kim-em committed 4 years ago

2689c517

chore(algebra/associated): weaken some typeclass assumptions (#7760)

Ruben-VandeVelde committed 4 years ago

4e7c6b27

feat(topology/connected): prod.totally_disconnected_space (#7747)

kim-em committed 4 years ago

8527efd1

Newer Older