leanprover-community/mathlib

Pull Requests Commits

feat(nat): add lemmas for multiplicity of gcd and lcm

unknown committed 3 years ago

dd05bc12

feat(data/polynomial/degree/definitions): if `r ≠ 0`, then `(monomial i r).nat_degree = i` (#14095)

adomani committed 3 years ago

c2e87de5

refactor(combinatorics/simple_graph/basic): relax `edge_finset` typeclasses (#14091)

kmill committed 3 years ago

59273305

feat(analysis/special_functions/pow): asymptotics for real powers and log (#14088)

b-mehta committed 3 years ago

41afd8c2

feat(data/complex): real exponential bounds (#14087)

b-mehta committed 3 years ago

1c8ce7e0

chore(topology/sequences): golf a few proofs (#14081)

urkud committed 3 years ago

b6d10283

feat(category_theory/noetherian): nonzero artinian objects have simple subobjects (#13972)

kim-em committed 3 years ago

7c4c90f4

chore(ring_theory/unique_factorization_domain): golf (#13820)

alreadydone committed 3 years ago

fd98cf15

feat(data/finsupp/basic): `finsupp.comap_domain` is an `add_monoid_hom` (#13783)

adomani committed 3 years ago

0c26348e

chore(analysis/special_functions/pow): golf a proof (#14093)

urkud committed 3 years ago

a9665571

feat(ring_theory/finiteness): tensor product of two finite modules is finite (#13733)

alreadydone committed 3 years ago

4977fd9d

feat(analysis/asymptotics): use weaker TC assumptions (#14080)

urkud committed 3 years ago

d4884c0d

chore(measure_theory/function/conditional_expectation): change the definition of condexp and its notation (#14010)

RemyDegenne committed 3 years ago

0302cfdd

feat(data/polynomial/laurent): add inductions for Laurent polynomials (#14005)

adomani committed 3 years ago

7a3ae977

feat(measure_theory/integral/interval_integral): add lemma `interval_integrable.sum` (#14069)

ocfnash committed 3 years ago

483affad

chore(algebra/module/submodule*): replace underscores in file names with a folder (#14063)

eric-wieser committed 3 years ago

83bc3b9c

chore(field_theory/adjoin): clarify and speed up proof (#14041)

Vierkantor committed 3 years ago

ba60237b

chore(set_theory/game/ordinal): Remove redundant namespaces (#14039)

vihdzp committed 3 years ago

b75113ac

feat(data/list): add a few lemmas (#14047)

urkud committed 3 years ago

4231b681

feat(topology/algebra/infinite_sum): lemmas about `mul_opposite` (#13674)

eric-wieser committed 3 years ago

df9683ca

refactor(algebra/{group,group_with_zero/basic): Delete lemmas generalized to division monoids (#14042)

YaelDillies committed 3 years ago

3ea573ef

chore({data/{finset,set},order/filter}/pointwise): Reorganize files (#14021)

YaelDillies committed 3 years ago

e6896117

chore(analysis/normed_space/basic): reorder the `restrict_scalars` definitions (#13995)

eric-wieser committed 3 years ago

45d2b523

feat(algebra/module/submodule_bilinear): add `submodule.map₂`, generalizing `submodule.has_mul` (#13709)

eric-wieser committed 3 years ago

91489acb

feat(topology/algebra/group): Division is an open map (#14028)

YaelDillies committed 3 years ago

34f29db3

move(order/synonym): Group `order_dual` and `lex` (#13769)

YaelDillies committed 3 years ago

c8926223

feat(analysis/convex/*): Convexity and subtraction (#14015)

YaelDillies committed 3 years ago

37c691f7

chore(.github/workflows): disable merge conflicts bot for now (#14057)

kim-em committed 3 years ago

56503664

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

leanprover-community-bot committed 3 years ago

153b20f5

fix(data/real/ennreal): style and golfing (#14055)

kbuzzard committed 3 years ago

b17070db

Older