leanprover-community/mathlib3

Pull Requests Commits

feat(combinatorics/simple_graph/connectivity): walk.copy function to relax dependent type issues (#15764)

kmill committed 3 years ago

734c95f1

feat(data/polynomial): some lemmas about (nat)degree of bit0/1 in char_zero (#15726)

alexjbest committed 3 years ago

678f62f0

feat(data/nat/factorization/prime_pow): lemmas relating `is_prime_pow` and `ord_compl = 1` (#15692)

stuart-presnell committed 3 years ago

aab6d3c7

refactor({data,linear_algebra}/matrix/block): Generalize block indexing (#14035)

YaelDillies committed 3 years ago

447cbe9c

chore(ring_theory/*): Fix lint (#16350)

YaelDillies committed 3 years ago

9556784a

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

Newer Older