leanprover-community/mathlib

Pull Requests Commits

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

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

chore(data/matrix/block): move block matrices into their own file (#8290)

eric-wieser committed 4 years ago

905b875e

feat(category_theory/monoidal): the definition of Tor (#7512)

kim-em committed 4 years ago

461130bc

feat(algebra/direct_sum): the submodules of an internal direct sum satisfy `supr A = ⊤` (#8274)

eric-wieser committed 4 years ago

b091c3fb

feat(ring_theory): (strict) monotonicity of `coe_submodule` (#8273)

Vierkantor committed 4 years ago

3a0ef3c2

chore(ring_theory): allow Dedekind domains to be fields (#8271)

Vierkantor committed 4 years ago

8be0eda2

chore(data/nat/prime): fix + add missing lemmas (#8066)

ericrbg committed 4 years ago

815e91f3

Newer Older