leanprover-community/mathlib3

Pull Requests Commits

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

PatrickMassot committed 5 years ago

25387b69

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

kim-em committed 5 years ago

f6f810cf

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

kim-em committed 5 years ago

6d2869ce

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

adamtopaz committed 5 years ago

79edde24

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

eric-wieser committed 5 years ago

84d27b45

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

eric-wieser committed 5 years ago

140e17b8

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

eric-wieser committed 5 years ago

51bc1ca4

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

urkud committed 5 years ago

93bc7e05

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

Vierkantor committed 5 years ago

52268b89

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

pechersky committed 5 years ago

a4d5ccb6

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

dwarn committed 5 years ago

94150f3a

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

dwarn committed 5 years ago

3a8796dd

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

Vierkantor committed 5 years ago

18af6b57

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

Vierkantor committed 5 years ago

1823aeef

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

eric-wieser committed 5 years ago

9b1b8543

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

jcommelin committed 5 years ago

bb9216c0

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

YaelDillies committed 5 years ago

78e36a71

Change the bors timeout to 8 hours (#7513)

eric-wieser committed 5 years ago

b765d4e7

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

eric-wieser committed 5 years ago

5a91d05e

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

riccardobrasca committed 5 years ago

37735250

chore(data/fintype): rework `fintype.equiv_fin` and dependencies (#7136)

Vierkantor committed 5 years ago

67dad976

chore(*): update to lean 3.30.0c (#7264)

gebner committed 5 years ago

048240e8

feat(category_theory/preadditive): Schur's lemma (#7366)

kim-em committed 5 years ago

7da83031

feat(data/finset/basic): a finset has card at most one iff it is contained in a singleton (#7404)

sgouezel committed 5 years ago

62c06a55

feat(topology/category): Profinite has colimits (#7434)

b-mehta committed 5 years ago

0cc3cd54

refactor(linear_algebra/eigenspace): refactor exists_eigenvalue (#7345)

kim-em committed 5 years ago

c7ba3dd0

chore(dynamics/periodic_pts): remove duplicate of nat.dvd_right_iff_eq (#7435)

Ruben-VandeVelde committed 5 years ago

58e990d9

feat(topology/category/Profinite): Any continuous bijection of profinite spaces is an isomorphism. (#7430)

adamtopaz committed 5 years ago

4bd1c836

feat(topology/discrete_quotient): Discrete quotients of topological spaces (#7425)

adamtopaz committed 5 years ago

30f3788c

feat(linear_algebra/char_poly): charpoly of `left_mul_matrix` (#7397)

Vierkantor committed 5 years ago

6d7e7563

Newer Older