leanprover-community/mathlib

Pull Requests Commits

docs(docs/undergrad): Update TODO list (#12752)

YaelDillies committed 4 years ago

351c32ff

feat(data/pfun): Remove unneeded assumption from pfun.fix_induction (#12920)

prakol16 committed 4 years ago

9ee02c6c

feat(order/category/FinBoolAlg): The category of finite Boolean algebras (#12906)

YaelDillies committed 4 years ago

3dd8e4d5

fix(combinatorics/simple_graph/density): correct name in docstring (#12921)

kmill committed 4 years ago

7ec1a31e

feat(combinatorics/simple_graph/{connectivity,metric}): `connected` and `dist` (#12574)

kmill committed 4 years ago

352ecfe1

feat(algebra/category/BoolRing): The category of Boolean rings (#12905)

YaelDillies committed 4 years ago

2891e1be

feat(model_theory/fraisse): Construct Fraïssé limits (#12138)

awainverse committed 4 years ago

f53b2399

feat(combinatorics/simple_graph/density): Edge density (#12431)

YaelDillies committed 4 years ago

6ac7c18d

feat(algebra/module/torsion): define torsion submodules (#12027)

pbazin committed 4 years ago

7302e116

chore(order/zorn): Review (#12175)

YaelDillies committed 4 years ago

c7745b3b

feat(topology/algebra/group): define `has_continuous_inv` and `has_continuous_neg` type classes (#12748)

j-loreaux committed 4 years ago

7c48d65c

feat(ring_theory/polynomial): mv_polynomial over UFD is UFD (#12866)

alreadydone committed 4 years ago

eabc6192

feat(*): facts about degrees/multiplicites of derivatives (#12856)

ericrbg committed 4 years ago

db760640

chore(data/polynomial/*): delete, rename and move lemmas (#12852)

astrainfinita committed 4 years ago

355645e3

feat(algebra/associated): generalize nat.prime_mul_iff (#12850)

Ruben-VandeVelde committed 4 years ago

c1fb0ed9

feat(data/list/basic): nth_le+filter lemmas (#12836)

ericrbg committed 4 years ago

a5a0d233

feat(model_theory/*): Facts about countability of first-order structures (#12819)

awainverse committed 4 years ago

892e6113

feat(number_theory/arithmetic_function): The moebius function is multiplicative (#12796)

khwilson committed 4 years ago

e6c6f006

chore(fintype/card_embedding): generalize instances (#12775)

ericrbg committed 4 years ago

0faebd2a

feat(number_theory/function_field): add completion with respect to place at infinity (#12715)

mariainesdff committed 4 years ago

04274301

feat(topology/nhds_set): add `has_basis_nhds_set` (#12908)

urkud committed 4 years ago

ca93096b

feat(measure_theory/integral): continuous functions with exponential decay are integrable (#12539)

loefflerd committed 4 years ago

399ce38e

feat(ring_theory/principal_ideal_domain): add some irreducible lemmas (#12903)

Ruben-VandeVelde committed 4 years ago

df348164

refactor(category_theory/abelian): trivial generalisations (#12897)

kim-em committed 4 years ago

a9781152

chore(topology/separation): move a lemma, golf (#12896)

urkud committed 4 years ago

d4e27d0b

feat(topology/continuous_function/bounded): add `bounded_continuous_function.tendsto_iff_tendsto_uniformly` (#12894)

j-loreaux committed 4 years ago

e968b6d1

chore(data/set/intervals): golf, rename (#12893)

urkud committed 4 years ago

a370cf05

feat(topology/separation): generalize tendsto_const_nhds_iff to t1_space (#12883)

fpvandoorn committed 4 years ago

5ef365a3

docs(data/set/pairwise): Explain preference for `s.pairwise_disjoint id` (#12878)

YaelDillies committed 4 years ago

6696bdd9

feat(data/complex/is_R_or_C): generalize `is_R_or_C.proper_space_span_singleton` to all finite dimensional submodules (#12877)

eric-wieser committed 4 years ago

30449be1

Newer Older