Commits leanprover-community/mathlib

chore(category_theory): homogenise usage of notation for terminal objects (#8106)

TwoFX committed 4 years ago

5796783b

chore(measure_theory/measure_space): add missing `finite_measure` instances (#8214)

kex-y committed 4 years ago

bb5ab1e7

feat(algebra/lie/from_cartan_matrix): construction of a Lie algebra from a Cartan matrix (#8206)

ocfnash committed 4 years ago

41ec92ea

feat(data/multiset/basic): add_eq_union_iff_disjoint (#8173)

pechersky committed 4 years ago

126a7b6e

feat(analysis/normed_space/int): norms of (units of) integers (#8136)

jcommelin committed 4 years ago

29beb1f3

fix(tactic/core): add subst' (#8129)

fpvandoorn committed 4 years ago

89e18376

feat(measure_theory/measure_space): if `f` restricted to `s` is measurable, then `f` is `ae_measurable` wrt `μ.restrict s` (#8098)

ADedecker committed 4 years ago

47c7c016

refactor(algebra/ordered_group): another step in the `order` refactor -- ordered groups (#8060)

adomani committed 4 years ago

06f0d517

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

leanprover-community-bot committed 4 years ago

20d8e837

chore(category_theory/monad/algebra): lint and golf (#8160)

b-mehta committed 4 years ago

d7653b8d

doc(data/set/function): add set. prefixes for doc-gen (#8215)

eric-wieser committed 4 years ago

03c8904a

doc(*): add bold in doc strings for named theorems i.e. **mean value theorem** (#8182)

hmonroe committed 4 years ago

ec07293a

feat(category_theory/closed): Exponential ideals (#4930)

b-mehta committed 4 years ago

13999970

feat(geometry/manifold/algebra): `left_invariant_derivation` (#8108)

Nicknamen committed 4 years ago

98e8408a

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