leanprover-community/mathlib3

Pull Requests Commits

chore(data/matrix/basic): add lemmas about dot_product and mul_vec (#8325)

eric-wieser committed 4 years ago

4ae97924

feat(measure_theory/conditional_expectation): define condexp_L2, conditional expectation of L2 functions (#8324)

RemyDegenne committed 4 years ago

b577bb2c

feat(ring_theory/ideal): generalize two results from finset to multiset (#8320)

Vierkantor committed 4 years ago

79fbd465

feat(data/matrix/{basic, block}): missing lemmas on conj_transpose (#8303)

eric-wieser committed 4 years ago

a783a47c

feat(algebra/lie/cartan_matrix): define the exceptional Lie algebras (#8299)

ocfnash committed 4 years ago

66055ddf

feat(data/multiset): `<` on multisets is well-founded (#8319)

Vierkantor committed 4 years ago

bc1f1459

feat(analysis/normed_space/normed_group_hom): add equalizer (#8228)

riccardobrasca committed 4 years ago

0597b1dd

chore(algebra/*): make non-instance typeclasses reducible. (#8322)

eric-wieser committed 4 years ago

7e5be024

refactor(topology/category/Profinite): define Profinite as a subcategory of CompHaus (#8314)

b-mehta committed 4 years ago

e42af8da

feat(measure_theory/simple_func_dense): induction lemmas for Lp.simple_func and Lp (#8300)

hrmacbeth committed 4 years ago

e343609b

refactor(algebra/ordered_ring): use `mul_le_mul'` for `canonically_ordered_comm_semiring` (#8284)

urkud committed 4 years ago

19a156ae

feat(combinatorics/simple_graph): add maps and subgraphs (#8223)

hmonroe committed 4 years ago

e9b1fbd0

Merge branch 'master' into monotone_integrable

ADedecker committed 4 years ago

2ec5b0cb

Merge branch 'master' into integral_test

ADedecker committed 4 years ago

c41e564c

feat(group_theory/submonoid/operations): `add_equiv.of_left_inverse` to match `linear_equiv.of_left_inverse` (#8279)

eric-wieser committed 4 years ago

bcc35c75

refactor(geometry/manifold): split `bump_function` into 3 files (#8313)

urkud committed 4 years ago

375dd53e

chore(algebra/module/pi): add `pi.smul_def` (#8311)

urkud committed 4 years ago

5bac21a1

feat(algebraic_topology/topological_simplex): This defines the natural functor from Top to sSet. (#8305)

adamtopaz committed 4 years ago

7fccf40a

feat(measure_theory/integration): if a function has bounded integral on all sets of finite measure, then it is integrable (#8297)

RemyDegenne committed 4 years ago

7d53431e

feat(normed_space): controlled_sum_of_mem_closure (#8310)

PatrickMassot committed 4 years ago

3b7e7bd6

chore(analysis/special_functions/pow): golf a few proofs (#8308)

urkud committed 4 years ago

2e9aa839

chore(algebra/big_operators/basic): spaces around binders (#8307)

YaelDillies committed 4 years ago

743209ca

feat(algebra/pointwise): `smul_comm_class` instances for `set` (#8292)

Vierkantor committed 4 years ago

e6731de1

refactor(measure_theory/measure_space): use `covariant_class` instead of `add_le_add` (#8285)

urkud committed 4 years ago

656722c5

feat(measure_theory/borel_space): a monotone function is measurable (#8045)

ADedecker committed 4 years ago

51cc43ef

chore(algebra/big_operators/basic): rename sum_(nat/int)_cast and (nat/int).coe_prod (#8264)

YaelDillies committed 4 years ago

8e5af430

doc(*): bold a few more named theorems (#8252)

hmonroe committed 4 years ago

4709e615

feat(data/int): conditionally complete linear order (#8149)

fpvandoorn committed 4 years ago

5021c1f9

feat(data/matrix/basic): add conj_transpose (#8291)

l534zhan committed 4 years ago

29b63a7e

feat(group_theory/free_product): the free product of an indexed family of monoids (#8256)

dwarn committed 4 years ago

63266ff4

Newer Older