leanprover-community/mathlib

Pull Requests Commits

feat(linear_map): to_*_linear_map_injective (#7746)

kim-em committed 4 years ago

abe146f7

feat(linear_algebra/tensor_product): Add is_scalar_tower instances (#6741)

eric-wieser committed 4 years ago

88685b03

feat(algebraic_topology/cech_nerve): The Cech nerve is a right adjoint. (#7716)

adamtopaz committed 4 years ago

31ba155f

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

leanprover-community-bot committed 4 years ago

272a930a

chore(order/pilex): add docstring (#7769)

YaelDillies committed 4 years ago

4c2bfdeb

feat(algebra/homology): i-th component of a chain map as a →+ (#7743)

kim-em committed 4 years ago

a8f5cc19

feat(data/finset): provide the coercion `finset α → Type*` (#7575)

Vierkantor committed 4 years ago

bec3e595

feat(data/finset/powerset): ssubsets and decidability (#7543)

agjftucker committed 4 years ago

ca740b64

chore(order/lexicographic): add module docstring (#7768)

YaelDillies committed 4 years ago

d2723432

chore(order/zorn): add module docstring (#7767)

YaelDillies committed 4 years ago

033a131a

feat(ring_theory/laurent_series): Defines Laurent series and their localization map (#7604)

awainverse committed 4 years ago

d0ebc8ef

feat(topology/semicontinuous): semicontinuity of compositions (#7763)

sgouezel committed 4 years ago

4555798c

feat(linear_algebra): the determinant of an endomorphism (#7635)

Vierkantor committed 4 years ago

2af69127

feat(algebra/homology): projective resolutions (#7486)

kim-em committed 4 years ago

7fe456d8

feat(order/basic): add simp attribute on le_refl, zero_le_one and zero_lt_one (#7733)

sgouezel committed 4 years ago

1a92c0de

chore(data/list): extract sublists to a separate file (#7757)

kim-em committed 4 years ago

fd48ac55

feat(analysis/normed_space): ∥n • a∥ ≤ n * ∥a∥ (#7745)

kim-em committed 4 years ago

14b597c3

fix(order/closure): unincorporated reviewer comments from #7446 (#7761)

fpvandoorn committed 4 years ago

0d842f08

refactor(convex/basic): make convex_hull into a closure operator (#7446)

YaelDillies committed 4 years ago

33d803aa

chore(data/fintype/basic): `fintype α/β` from `fintype α ⊕ β` (#7736)

ericrbg committed 4 years ago

25e36bea

feat(measure_theory/integration): in a sigma finite space, there exists an integrable positive function (#7721)

sgouezel committed 4 years ago

4ea253b7

feat(algebra/homology): complexes in functor categories (#7744)

kim-em committed 4 years ago

8e25bb6c

feat(algebra/homology): construct isomorphisms of complexes (#7741)

kim-em committed 4 years ago

f4d145ee

chore(ring_theory/hahn_series): extract lemmas from slow definitions (#7737)

eric-wieser committed 4 years ago

08bb1125

feat(src/ring_theory/derivation): merge duplicates `derivation.comp` and `linear_map.comp_der` (#7727)

ocfnash committed 4 years ago

e2168e55

feat(topology/continuous_function/algebra): add `coe_fn_(linear_map|ring_hom|alg_hom)` (#7720)

eric-wieser committed 4 years ago

9d63c388

feat(algebra/homology): eval and forget functors (#7742)

kim-em committed 4 years ago

a3ba4d47

feat(analysis/normed_space): SemiNormedGroup.has_zero_object (#7740)

kim-em committed 4 years ago

035aa60b

chore(category_theory): dualize filtered categories to cofiltered categories (#7731)

kim-em committed 4 years ago

1ac49b0e

chore(linear_algebra/finsupp): remove useless lemma (#7734)

kim-em committed 4 years ago

f74a3753

Newer Older