Commits leanprover-community/mathlib

Start on computing Ext^1(Z/2,Z/2)

jcommelin committed 4 years ago

1b3faca5

feat(category_theory/abelian/ext): Defines Ext functors. (#8186)

kim-em committed 4 years ago

23d22e4a

chore(measure_theory/decomposition): change statement to use the `finite_measure` instance (#8207)

kex-y committed 4 years ago

2f720232

feat(algebra/invertible): construction from is_unit (#8205)

eric-wieser committed 4 years ago

6365c6c1

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

leanprover-community-bot committed 4 years ago

27841bbb

feat(linear_algebra/nonsingular_inverse): add lemmas about `invertible` (#8201)

eric-wieser committed 4 years ago

77e1e3b2

feat(category_theory/linear/yoneda): A linear version of Yoneda. (#8199)

adamtopaz committed 4 years ago

9d998338

feat(measure_theory/lp_space): define the Lp function corresponding to the indicator of a set (#8193)

RemyDegenne committed 4 years ago

b6bf7a30

feat(topology/instances/ennreal): add tsum lemmas for ennreal.to_real (#8184)

kex-y committed 4 years ago

7eab080b

feat(algebra/to_additive): map pow to smul (#7888)

fpvandoorn committed 4 years ago

38a6f265

feat(category_theory/preadditive/opposite): Adds some instances and lemmas (#8202)

adamtopaz committed 4 years ago

f2edc5a3

refactor(ring_theory): turn `localization_map` into a typeclass (#8119)

Vierkantor committed 4 years ago

0b0d8e7e

feat(ring_theory/trace): the composition of `trace`s is `trace` (#8078)

Vierkantor committed 4 years ago

6bad4c61

chore(algebra/invertible): units coerced to their monoid are invertible (#8195)

eric-wieser committed 4 years ago

8ba94ab7

feat(linear_algebra/matrix/reindex): generalize reindex_linear_equiv to operate on an arbitrary ring (#8159)

eric-wieser committed 4 years ago

63c8d333

feat(algebra/lie/free): the universal enveloping algebra of the free Lie algebra is the free associative algebra (#8183)

ocfnash committed 4 years ago

a8f60ebc

feat(measure_theory/conditional_expectation): define the Lp subspace of functions measurable wrt a sigma-algebra, prove completeness (#7945)

RemyDegenne committed 4 years ago

4ace3b73

chore(category_theory/abelian/diagram_lemmas/four): Make the diagram into a code block (#8192)

shingtaklam1324 committed 4 years ago

01b062a1

feat(data/finset/basic): sdiff_val, disjoint_to_finset_iff_disjoint (#8168)

pechersky committed 4 years ago

d819e364

doc(measure_theory/measurable_space): correct tiny misprints in two doc-strings (#8187)

kkytola committed 4 years ago

2ebd96c2

chore(data/list/perm): make `perm_nil` a simp lemma (#8191)

eric-wieser committed 4 years ago

7135c96f

chore(measure_theory/{bochner_integration, simple_func_dense}): Move construction of embedding of L1 simple funcs (#8185)

hrmacbeth committed 4 years ago

a9db7ced

ci(.github/workflows/*): switch to self-hosted runners (#8177)

bryangingechen committed 4 years ago

180d004c

feat(data/list/basic): map_permutations (#8188)

digama0 committed 4 years ago

863f0075

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

leanprover-community-bot committed 4 years ago

cdb44dfa

feat(category_theory): left-derived functors (#7487)

kim-em committed 4 years ago

531d8504

refactor(measure_theory/simple_func_dense): generalize approximation results from L^1 to L^p (#8114)

hrmacbeth committed 4 years ago

74a0f67b

feat(algebra/invertible): add a missing lemma `inv_of_eq_left_inv` (#8179)

l534zhan committed 4 years ago

a022bb75

feat(group_theory/perm/basic): of_subtype_apply_of_mem (#8174)

pechersky committed 4 years ago

111ac5ca

feat(algebra/periodic): a few more periodicity lemmas (#8062)

benjamindavidson committed 4 years ago

25d042c1