leanprover-community/mathlib

Pull Requests Commits

feat(category_theory/.../zero): if a zero morphism is a mono, the source is zero (#7462)

kim-em committed 4 years ago

6af5fbd2

feat(measure_theory/set_integral): continuous_on.measurable_at_filter (#7511)

benjamindavidson committed 4 years ago

009be861

feat(category_theory/Fintype): some lemmas and `Fintype_to_Profinite`. (#7491)

adamtopaz committed 4 years ago

709c73b2

feat(data/finsupp): prove `f.curry x y = f (x, y)` (#7475)

Vierkantor committed 4 years ago

1ef04bde

feat(algebra/big_operators): telescopic sums (#7470)

PatrickMassot committed 4 years ago

d3a46a7f

feat(order/filter_at_top_bot): extraction lemmas (#7469)

PatrickMassot committed 4 years ago

18ada66c

feat(category_theory/subobject): minor tweaks (#7466)

kim-em committed 4 years ago

7cc367b7

feat(category_theory/quotient): the quotient functor is full and essentially surjective (#7465)

kim-em committed 4 years ago

e25cbe0d

feat(category_theory/preadditive): reformulation of mono_of_kernel_zero (#7464)

kim-em committed 4 years ago

19b752c4

feat(category_theory/.../additive_functor): additive functors preserve zero objects (#7463)

kim-em committed 4 years ago

77949694

docs(overview): Add Stone-Weierstrass (#7449)

PatrickMassot committed 4 years ago

25387b69

doc(algebraic_hierarchy): advice for adding new typeclasses (#6854)

kim-em committed 4 years ago

f6f810cf

feat(category_theory/.../images): image.pre_comp_epi_of_epi (#7460)

kim-em committed 4 years ago

6d2869ce

feat(topology/discrete_quotient): Add a few lemmas about discrete quotients (#7454)

adamtopaz committed 4 years ago

79edde24

refactor(group_theory/group_action/defs): generalize smul_mul_assoc and mul_smul_comm (#7441)

eric-wieser committed 4 years ago

84d27b45

feat(algebra/direct_sum_graded): a direct_sum of copies of a ring is itself a ring (#7420)

eric-wieser committed 4 years ago

140e17b8

feat(algebra/direct_sum_graded): add direct_sum.to_semiring (#7380)

eric-wieser committed 4 years ago

51bc1ca4

feat(order): add some missing `pi` and `Prop` instances (#7268)

urkud committed 4 years ago

93bc7e05

feat(linear_algebra): Vandermonde matrices and their determinant (#7116)

Vierkantor committed 4 years ago

52268b89

chore(order/complete_boolean_algebra): speed up Inf_sup_Inf (#7506)

pechersky committed 4 years ago

a4d5ccb6

chore(group_theory/nielsen_schreier): typos in module doc-string (#7500)

dwarn committed 4 years ago

94150f3a

feat(category_theory/path_category): extensionality for functors out of path category (#7494)

dwarn committed 4 years ago

3a8796dd

feat(algebra/module): `linear_equiv.refl.symm = refl` (#7493)

Vierkantor committed 4 years ago

18af6b57

feat(algebra/module): `S`-linear equivs are also `R`-linear equivs (#7476)

Vierkantor committed 4 years ago

1823aeef

feat(data/fintype/basic): add set.to_finset_range (#7426)

eric-wieser committed 4 years ago

9b1b8543

feat(category_theory/opposites): iso.unop (#7400)

jcommelin committed 4 years ago

bb9216c0

feat(analysis/convex/extreme): extreme sets (#7357)

YaelDillies committed 4 years ago

78e36a71

Change the bors timeout to 8 hours (#7513)

eric-wieser committed 4 years ago

b765d4e7

feat(data/finset/lattice): add sup_image (#7428)

eric-wieser committed 4 years ago

5a91d05e

feat(ring_theory/finiteness): add lemmas (#7409)

riccardobrasca committed 4 years ago

37735250

Newer Older