leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' into adomani_regular_inj_dot_notation

adomani committed 3 years ago

1a33d650

chore(algebra/regular/basic): clean up variables and slight golf (#16321)

adomani committed 3 years ago

f84386d7

feat(topology/instances/ennreal): `ennreal.to_nnreal` applied to a `tsum` (#16320)

dtumad committed 3 years ago

17ff82d9

feat(logic/basic): `function.mt` and `function.mtr` (#16315)

kmill committed 3 years ago

b35461b8

chore(topology/algebra/order/basic): deduplicate (#16287)

urkud committed 3 years ago

6a68f86a

feat(order/locally_finite): transfer locally_finite_order across order_iso (#16264)

gebner committed 3 years ago

386acbac

feat(data/finset/locally_finite): more on `filter (< c)` (#16260)

gebner committed 3 years ago

70c48638

adomani committed 3 years ago

d5ec4534

Merge branch 'adomani_regular_variables' into adomani_regular_inj_dot_notation

adomani committed 3 years ago

f71496b4

Merge branch 'master' into adomani_regular_inj_dot_notation

adomani committed 3 years ago

09c8b5f5

refactor(algebra/monoid_algebra/{ basic + support } + import dust): move lemmas to a new "support" file (#16322)

adomani committed 3 years ago

20cfd341

feat(analysis/complex/basic): add `complex.ring_hom_eq_id_or_conj_of_continuous` (#16169)

xroblot committed 3 years ago

489c1c57

feat(order/filter/basic): add `eventually_le.add_le_add` (#16295)

kex-y committed 3 years ago

f5da0822

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

leanprover-community-bot committed 3 years ago

5083718c

chore(.github/workflows): increase olean generation timeout (#15784)

collares committed 3 years ago

13618c1c

feat(category_theory/limits): (co)limits in full subcategories (#16188)

TwoFX committed 3 years ago

fe5e4ce6

clean up variables and slight golf

adomani committed 3 years ago

ea369969

use variables of the file

adomani committed 3 years ago

9337677b

feat(probability/hitting_time): add some hitting time lemmas (#16296)

kex-y committed 3 years ago

002aa517

feat(data/polynomial/derivative): add more lemmas (#16139)

Ruben-VandeVelde committed 3 years ago

1da31fac

adomani committed 3 years ago

c567ac25

left/right_regular.inj

adomani committed 3 years ago

f907109e

chore(analysis, measure_theory): Fix lint (#16216)

YaelDillies committed 3 years ago

d003c550

chore(*): bump to lean 3.47.0 (#16252)

digama0 committed 3 years ago

3d7987cd

feat(linear_algebra/finite_dimensional): `dim_add_le_dim_add_dim` (#16301)

jsm28 committed 3 years ago

fbfe26dc

feat(algebraic_topology): the category simplicial_object.split (#16274)

joelriou committed 3 years ago

86e93623

feat(category_theory/adjunction): the Special Adjoint Functor Theorem (#15987)

TwoFX committed 3 years ago

c82fab81

feat(data/list/rdrop): drop or take from the right (#15475)

pechersky committed 3 years ago

ed231516

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

leanprover-community-bot committed 3 years ago

3683b34a

feat(ring_theory/unique_factorization_domain): add `associated_iff_normalized_factors_eq_normalized_factors` (#16221)

astrainfinita committed 3 years ago

20f94541

Older