leanprover-community/mathlib3

Pull Requests Commits

feat(data/nat/enat): derive typeclasses about well founded (#16346)

astrainfinita committed 3 years ago

8bedeafb

feat(category_theory/limits/has_limits): `const` and `(co)lim` are adjoint (#16251)

jjaassoonn committed 3 years ago

62f14c33

feat(set_theory/cardinal/finite): `nat.card_pi` (#16143)

tb65536 committed 3 years ago

1555e3de

refactor(data/list/forall2): consistent names of relations (#16098)

madvorak committed 3 years ago

d6789b8b

feat(topology/separation): `embedding.discrete_topology` (#16092)

tb65536 committed 3 years ago

3c927487

chore(analysis/box_integral): use GP instead of bot (#15939)

urkud committed 3 years ago

09fb38cc

feat(data/rat/defs): inv_coe_{int,nat}_{num,denom} (#15863)

pechersky committed 3 years ago

86152105

feat(geometry/euclidean/oriented_angle): signs of angles between linear combinations of vectors (#16243)

jsm28 committed 3 years ago

ddc74844

chore(topology/order): open `function`, don't open `classical` (#16288)

urkud committed 3 years ago

541b2880

feat(topology/fiber_bundle): Each fiber of a trivialization is homeomorphic to the specified fiber (#16079)

tb65536 committed 3 years ago

525c5a81

feat(measure_theory/integral/bochner): Hölder's inequality for real nonnegative functions (#16291)

RemyDegenne committed 3 years ago

394f6e63

feat(data/finsupp/lex): lexicographic orders on finsupps and covariant classes (#16127)

adomani committed 3 years ago

44c94be8

feat(data/finset/basic): Add `coe_pair` lemmas (#16235)

linesthatinterlace committed 3 years ago

8d90fcdb

chore(data/real/nnreal): Golf (#16307)

YaelDillies committed 3 years ago

370cc484

feat(data/sign): Allocating signs (#14335)

YaelDillies committed 3 years ago

616e6ef3

refactor(topology/algebra/continuous_monoid_hom): Make variables consistent (#16304)

tb65536 committed 3 years ago

9b68ed5e

feat(*): bump to lean 3.48.0 (#16292)

gebner committed 3 years ago

acbe099c

doc(measure_theory/integral): integrability docstrings (#16269)

mcdoll committed 3 years ago

87d8c4b3

chore(algebra/divisibility): golf (#16327)

astrainfinita committed 3 years ago

371b4143

refactor(group_theory/subgroup/basic): Make `subgroup.opposite` an `equiv` (#16271)

YaelDillies committed 3 years ago

5b7bc676

feat(probability/independence): add indep_bot_left and indep_bot_right (#16309)

RemyDegenne committed 3 years ago

39014ec9

feat(order/filter/small_sets): yet another squeeze theorem (#16286)

urkud committed 3 years ago

5a3cd16b

feat(algebra/invertible): `map_inv_of` and some other basic results (#16202)

eric-wieser committed 3 years ago

5e194d48

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

Newer Older