leanprover-community/mathlib

Pull Requests Commits

feat(logic/nontrivial): `exists_pair_lt` (#12925)

vihdzp committed 3 years ago

023a7838

feat(set_theory/cardinal_ordinal): `κ ^ n = κ` for infinite cardinals (#12922)

vihdzp committed 3 years ago

c51f4f10

feat(topology/instances/ennreal): add `ennreal.has_sum_to_real` (#12926)

urkud committed 3 years ago

9d26041f

feat(linear_algebra/sesquilinear_form): add nondegenerate (#12683)

mcdoll committed 3 years ago

b83bd25d

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

ADedecker committed 3 years ago

ebdd3b5c

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

Newer Older