leanprover-community/mathlib3

Pull Requests Commits

chore(algebra/order/absolute_value): superficial tidying (#16190)

ericrbg committed 3 years ago

76be8c73

feat(topology/sheaves/sheaf_condition): Description of sections on the union of two open sets. (#16093)

erdOne committed 3 years ago

27d83241

feat(category_theory/adjunction): complete well-powered category with a coseparating set is cocomplete (#15988)

TwoFX committed 3 years ago

361aa777

feat(linear_algebra/affine_space/finite_dimensional): `insert` lemmas (#16308)

jsm28 committed 3 years ago

865184b4

chore(topology/instances/rat): add `namespace rat` (#16306)

urkud committed 3 years ago

07190764

feat(logic/equiv/option): equivalence with subtypes (#16302)

jsm28 committed 3 years ago

1e91718f

refactor(analysis/convex/cone): move cone.lean to cone/basic.lean (#16270)

apurvnakade committed 3 years ago

d44692a8

feat(algebra/gcd_monoid): `simp` lemmas for `associated (normalize x) y` (#16249)

Vierkantor committed 3 years ago

2d30ffcf

feat(algebra/order/smul): `ordered_smul` instances for `ℕ` and `ℤ` (#16247)

YaelDillies committed 3 years ago

eaa51e72

feat(algebraic_topology/dold_kan): the normalized Moore complex is homotopy equivalent to the alternating face map complex (#16246)

joelriou committed 3 years ago

f951e201

feat(algebra/category/Module/change_of_rings): extension of scalars (#15673)

jjaassoonn committed 3 years ago

9e274549

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

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

urkud committed 3 years ago

8012ac97

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

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

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

Newer Older