leanprover-community/mathlib3

Pull Requests Commits

the conformal inversion map

justadzr committed 4 years ago

593e627e

chore(algebra/order/sub): generalize 2 lemmas (#9611)

urkud committed 4 years ago

9ecdd380

feat(algebra/order/ring): variants of mul_sub' (#9604)

fpvandoorn committed 4 years ago

639a7ef4

feat(data/nat/log): add antitonicity lemmas for first argument (#9597)

jchoules committed 4 years ago

83a07ce0

feat(data/multiset/interval): Intervals as `multiset`s (#9588)

YaelDillies committed 4 years ago

41dd4da3

refactor(data/multiset/basic): remove sub lemmas (#9578)

fpvandoorn committed 4 years ago

c3768cc8

feat(algebra/module/basic): `module rat E` is a subsingleton (#9570)

urkud committed 4 years ago

c4006779

move(order/*): move from `algebra.order.` the files that aren't about algebra (#9562)

YaelDillies committed 4 years ago

eb3595ed

feat(group_theory/subgroup/basic): Analog of `mul_aut.conj` for normal subgroups. (#9552)

tb65536 committed 4 years ago

8aa18938

feat(analysis/convex/function): API for strict convex functions (#9437)

YaelDillies committed 4 years ago

1390b447

refactor(data/*/interval): generalize `finset.Ico` to locally finite orders (#7987)

YaelDillies committed 4 years ago

a0504eb3

feat(ring_theory/coprime): two lemmas prereq for #8611 (#9456)

hrmacbeth committed 4 years ago

ba2454e6

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

leanprover-community-bot committed 4 years ago

235bfd7e

fix(topology/path_connected): add `continuity` to `path.continuous_extend` (#9605)

shingtaklam1324 committed 4 years ago

9ea4568b

refactor(analysis/normed_space/linear_isometry): semilinear isometries (#9551)

dupuisf committed 4 years ago

fa3b6222

feat(topology/algebra): valued fields (#9589)

PatrickMassot committed 4 years ago

9518ce12

feat(measure_theory/covering/besicovitch): the measurable Besicovitch covering theorem (#9576)

sgouezel committed 4 years ago

ebccce9b

refactor(data/ennreal/basic): prove has_ordered_sub instance (#9582)

fpvandoorn committed 4 years ago

8a60fd75

feat(algebra/order/with_zero): add lt_of_mul_lt_mul_of_le₀ and mul_lt_mul_of_lt_of_le₀ (#9596)

alexjbest committed 4 years ago

bf76a1f2

feat(src/category_theory/*): Yoneda preserves limits. (#9580)

erdOne committed 4 years ago

18a42f3f

feat(data/multiset/erase_dup): Alias for `multiset.erase_dup_eq_self` (#9587)

YaelDillies committed 4 years ago

f8747832

feat(analysis/normed_space/add_torsor_bases): the interior of the convex hull of a finite affine basis is the set of points with strictly positive barycentric coordinates (#9583)

ocfnash committed 4 years ago

cc46f314

feat(category_theory/*): Yoneda extension is Kan (#9574)

erdOne committed 4 years ago

a7784aad

feat(analysis/asymptotics): Define superpolynomial decay of a function (#9440)

dtumad committed 4 years ago

b9097f11

fix(algebra/group/{prod,pi}): fix non-defeq `has_scalar` diamonds (#9584)

eric-wieser committed 4 years ago

0bc7c2d5

feat(category_theory/limits/*): Filtered colimits preserves finite limits (#9522)

erdOne committed 4 years ago

cb3c8448

feat(category_theory/limits/preserves/*): Show that whiskering left preserves limits. (#9581)

erdOne committed 4 years ago

7a2696d0

refactor(algebra/gcd_monoid): drop nontriviality assumptions (#9568)

Ruben-VandeVelde committed 4 years ago

f37aeb00

refactor(data/finsupp/basic): has_ordered_sub on finsupp (#9577)

fpvandoorn committed 4 years ago

f63786b9

feat(data/multiset/basic): has_ordered_sub multiset (#9566)

fpvandoorn committed 4 years ago

b4a97675

Older