leanprover-community/mathlib

Pull Requests Commits

bottine committed 3 years ago

79cdccf9

merging complete

bottine committed 3 years ago

f31491a7

bottine committed 3 years ago

b0579b69

merging changes from the subgroupoid commits

bottine committed 3 years ago

97b5ff2c

bottine committed 3 years ago

27574aeb

bottine committed 3 years ago

420da16d

Apply suggestions from code review

bottine committed 3 years ago

Verified 1f8ef487

Merge remote-tracking branch 'origin/master' into bottine/subgroupoid_more

bottine committed 3 years ago

72e0be65

bottine committed 3 years ago

a0328d06

chore(topology/sheaf_condition): is_sheaf_iff_pairwise_intersections without products (#17181)

alreadydone committed 3 years ago

20e597fb

chore(category_theory/groupoid/*) More subgroupoid lemmas (#17147)

bottine committed 3 years ago

14c11403

refactor(topology/bases): removing/adding the empty set from/to a basis (#17133)

alreadydone committed 3 years ago

dc2a9659

feat(analysis/calculus/uniform_limits_deriv): pointwise convergence out of derivative convergence on a preconnected set (#17123)

sgouezel committed 3 years ago

1a249186

feat(order/filter/ultrafilter): an ultrafilter is an atom in the lattice of filters (#17116)

urkud committed 3 years ago

c680de9e

feat(analysis/convex/side): connectedness of sides (#16938)

jsm28 committed 3 years ago

4b6fbb3e

feat(is_cyclotomic_extension/basic): add is_cyclotomic_extension.equiv (#16757)

riccardobrasca committed 3 years ago

1acf2b9a

feat(topology/sheaves/*): Notation for restriction of sections. (#16088)

erdOne committed 3 years ago

06c75afe

feat(data/nat/interval): Cauchy induction (#15880)

Shimonschlessinger committed 3 years ago

9340cc93

feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces (#16796)

ADedecker committed 3 years ago

bcf8d82b

feat({data, analysis}/complex/basic): lemmas related to `complex.partial_order` (#17170)

j-loreaux committed 3 years ago

05f9a362

feat(data/set/intervals/basic): Injectivity of half-infinite intervals (#17157)

mans0954 committed 3 years ago

438381a5

chore(data/set/pointwise): split file, reducing dependencies (#16950)

kim-em committed 3 years ago

aa329229

feat(algebra/order/floor): some nat.ceil lemmas (#16987)

alexjbest committed 3 years ago

ad7dca6a

docs(src/order/locally_finite.lean): fix a copy-paste typo (#17196)

adomani committed 3 years ago

192f43c6

feat(analysis/normed_space/star/gelfand_duality): realize the Gelfand transform as a `star_alg_equiv` (#17167)

j-loreaux committed 3 years ago

30415257

bottine committed 3 years ago

07d24a45

feat(algebra/group_power/order): add `pow_lt_self_of_lt_one` (#17162)

urkud committed 3 years ago

5118ae32

feat(data/fintype/basic): lemmas about `finset.univ` (#17067)

urkud committed 3 years ago

5155be47

merge changes from subgroupoid_more_less

bottine committed 3 years ago

f9289328

bottine committed 3 years ago

a3321e97

Older