leanprover-community/mathlib3

Pull Requests Commits

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

leanprover-community-bot committed 3 years ago

17b621c0

feat(topology/continuous_function/cocompact_maps): add the type of cocompact continuous maps (#12938)

j-loreaux committed 3 years ago

b6d246a6

feat(topology/metric_space/metrizable): define and use a metrizable typeclass (#12934)

sgouezel committed 3 years ago

221796ab

chore(nnreal): rename lemmas based on real.to_nnreal when they mention of_real (#12937)

sgouezel committed 3 years ago

5925650f

feat(topology/category/Born): The category of bornologies (#12045)

YaelDillies committed 3 years ago

21435715

move(algebra/hom/*): Move group hom files together (#12647)

YaelDillies committed 3 years ago

172f3179

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

YaelDillies committed 3 years ago

351c32ff

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

prakol16 committed 3 years ago

9ee02c6c

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

YaelDillies committed 3 years ago

3dd8e4d5

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

kmill committed 3 years ago

7ec1a31e

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

kmill committed 3 years ago

352ecfe1

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

YaelDillies committed 3 years ago

2891e1be

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

awainverse committed 3 years ago

f53b2399

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

YaelDillies committed 3 years ago

6ac7c18d

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

pbazin committed 3 years ago

7302e116

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

YaelDillies committed 3 years ago

c7745b3b

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

j-loreaux committed 3 years ago

7c48d65c

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

alreadydone committed 3 years ago

eabc6192

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

ericrbg committed 3 years ago

db760640

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

astrainfinita committed 3 years ago

355645e3

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

Ruben-VandeVelde committed 3 years ago

c1fb0ed9

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

ericrbg committed 3 years ago

a5a0d233

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

awainverse committed 3 years ago

892e6113

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

khwilson committed 3 years ago

e6c6f006

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

ericrbg committed 3 years ago

0faebd2a

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

mariainesdff committed 3 years ago

04274301

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

urkud committed 3 years ago

ca93096b

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

loefflerd committed 3 years ago

399ce38e

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

Ruben-VandeVelde committed 3 years ago

df348164

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

kim-em committed 3 years ago

a9781152

Newer Older