leanprover-community/mathlib

Pull Requests Commits
refactor(algebra/invertible): push deeper into the import graph (#6650)
eric-wieser committed 5 years ago
f54f81c0
feat(measure_theory/lp_space): Lp is complete (#6563)
sgouezel committed 5 years ago
85c6a799
feat(data/polynomial/*): more lemmas, especially for noncommutative rings (#6599)
kim-em committed 5 years ago
dae047ed
chore(scripts): update nolints.txt (#6651)
leanprover-community-bot committed 5 years ago
b8526489
feat(.docker): Docker containers for debian, alpine, and gitpod (#6515)
kim-em committed 5 years ago
2dabe5af
fix (topology/algebra/basic): fix universe issue with of_nhds_one (#6647)
kbuzzard committed 5 years ago
b1aafb20
guess
eric-wieser committed 5 years ago
391ad51e
Add a missing lemma about alg_equiv conversions
eric-wieser committed 5 years ago
a27742c1
Eliminate a slow convert
eric-wieser committed 5 years ago
e2721ab3
Fill in an "underscore"
eric-wieser committed 5 years ago
38a38990
fill in difficult underscore
eric-wieser committed 5 years ago
0f0b4ebe
feat(data/multiset/basic): Multiset induction lemma (#6623)
tb65536 committed 5 years ago
4d8d344c
feat(data/complex/is_R_or_C): add linear maps for is_R_or_C.re, im, conj and of_real (#6621)
RemyDegenne committed 5 years ago
bd3695ac
feat(topology/algebra/infinite_sum): add `tsum_even_add_odd` (#6620)
urkud committed 5 years ago
998a3827
refactor(data/{,mv_}polynomial): support function (#6615)
gebner committed 5 years ago
95a8e958
feat(topology/algebra/ordered): generalize `real.compact_Icc` (#6602)
urkud committed 5 years ago
f5c9d0f4
tidy
eric-wieser committed 5 years ago
f14ccfb7
refactor(module/submodule): allow submodules to be used for sub-distrib_mul_actions
eric-wieser committed 5 years ago
ee7eedd2
fix(normed_space/multilinear): speed up slow proof (#6639)
robertylewis committed 5 years ago
3b3a8b55
chore(tactic/interactive): propagate tags in `substs` (#6638)
eric-wieser committed 5 years ago
3d451c70
feat(group_theory/subgroup): le_ker_iff (#6630)
tb65536 committed 5 years ago
9beec03c
refactor(data/polynomial/degree/definitions): Remove hypothesis of nat_degree_X_pow_sub_C (#6628)
tb65536 committed 5 years ago
57fda28f
feat(field_theory/polynomial_galois_group): ext lemma (#6627)
tb65536 committed 5 years ago
41f11966
feat(group_theory/solvable): Commutative groups are solvable (#6625)
tb65536 committed 5 years ago
3dd12573
feat(field_theory/splitting_field): splits_pow (#6624)
tb65536 committed 5 years ago
2c4a9855
refactor(topology): make is_closed a class (#6552)
sgouezel committed 5 years ago
653fd292
feat(measure_theory/pi_system) lemmas for pi_system, useful for independence. (#6353)
mzinkevi committed 5 years ago
56065f7e
feat(linear_algebra/basic): add missing lemma finsupp.sum_smul_index_linear_map' (#6565)
ocfnash committed 5 years ago
925ea07d
chore(geometry/manifold): use notation `𝓘(𝕜, E)` (#6636)
urkud committed 5 years ago
b7c5709d
chore(scripts): update nolints.txt (#6635)
leanprover-community-bot committed 5 years ago
514973a9
Terms Of Use Privacy Policy Refund Policy Impressum