leanprover-community/mathlib3

Pull Requests Commits

chore(data/nat/multiplicity): simplify proof (#14103)

ChrisHughes24 committed 3 years ago

0e834dfe

fix(analysis/special_functions/pow): fix norm_num extension (#14099)

digama0 committed 3 years ago

0509c9c6

chore(data/polynomial/ring_division): golf a few proofs (#14097)

urkud committed 3 years ago

c8edd608

chore(order/filter/basic): golf a few proofs (#14078)

urkud committed 3 years ago

6cf6e8cb

feat(data/polynomial/laurent): add truncation from Laurent polynomials to polynomials (#14085)

adomani committed 3 years ago

9b41e4e0

chore(order/complete_lattice,data/set/lattice): move `Sup_sUnion` (#14077)

urkud committed 3 years ago

fa4c0368

feat(data/multiset/basic): `erase_singleton` (#14094)

alreadydone committed 3 years ago

bada932c

chore(set_theory/zfc): use `derive` for some instances (#14079)

urkud committed 3 years ago

55671bee

feat(algebra/*): Division monoid instances for `with_zero` and `mul_opposite` (#14073)

YaelDillies committed 3 years ago

d9e623c2

feat({data/{finset,set},order/filter}/pointwise): Pointwise monoids are division monoids (#13900)

YaelDillies committed 3 years ago

c57cfc6d

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

Newer Older