leanprover-community/mathlib

Pull Requests Commits

feat(algebra/algebra/basic): support algebra towers in endomorphism_algebra

eric-wieser committed 4 years ago

6916aef0

chore(algebra/algebra/basic): golf endomorphism_algebra

eric-wieser committed 4 years ago

4063c236

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

chore(probability_theory/integration): style changes. Make arguments implicit, remove spaces, etc. (#8286)

RemyDegenne committed 4 years ago

bf868344

feat(linear_algebra/finsupp): mem_supr_iff_exists_finset (#8268)

eric-wieser committed 4 years ago

f1e27d29

chore(data/set/intervals): relax linear_order to preorder in the proofs of `Ixx_eq_empty_iff` (#8071)

YaelDillies committed 4 years ago

3e56439d

chore(data/mv_polynomial/basic): use `is_empty σ` instead of `¬nonempty σ` (#8277)

eric-wieser committed 4 years ago

bb53a922

feat(geometry/manifold): add `charted_space` and `model_with_corners` for pi types (#6578)

urkud committed 4 years ago

dd9a0ea2

refactor(topology/metric/gromov_hausdorff_realized): speed up a proof (#8287)

sgouezel committed 4 years ago

7bed785b

feat(topology/algebra/ordered/basic): basis for the neighbourhoods of `top`/`bot` (#8283)

hrmacbeth committed 4 years ago

f1f40840

feat(measure_theory/l2_space): the inner product of indicator_const_Lp and a function is the set_integral (#8229)

RemyDegenne committed 4 years ago

f302c979

chore(topology/topological_fiber_bundle): renaming (#8270)

Nicknamen committed 4 years ago

9dfb9a6e

feat(measure_theory/measure_space): add `finite_measure_sub` instance (#8239)

kex-y committed 4 years ago

cde57482

feat(measure_theory/integration): add `lintegral_union` (#8238)

kex-y committed 4 years ago

5ea9a073

refactor(measure_theory/simple_func_dense): generalize L1.simple_func.dense_embedding to Lp (#8209)

hrmacbeth committed 4 years ago

4cd6179c

docs(data/rel): add module docstring (#8248)

YaelDillies committed 4 years ago

a9cb722c

feat(algebra/opposites): functoriality of the opposite monoid (#8254)

dwarn committed 4 years ago

a2b00f3c

feat(ring_theory): `coe_submodule S (⊤ : ideal R) = 1` (#8272)

Vierkantor committed 4 years ago

6fa678fb

feat(data/equiv/fin): fin_order_iso_subtype (#8258)

pechersky committed 4 years ago

0a8e3eda

feat(data/list/basic): more lemmas about permutations_aux2 (#8198)

eric-wieser committed 4 years ago

66cc624c

feat({data,linear_algebra}/{finsupp,dfinsupp}): add `{add_submonoid,submodule}.[d]finsupp_sum_mem` (#8269)

eric-wieser committed 4 years ago

695cb07b

Older