leanprover-community/mathlib3

Pull Requests Commits

refactor(algebra/invertible): push deeper into the import graph (#6650)

eric-wieser committed 4 years ago

f54f81c0

feat(measure_theory/lp_space): Lp is complete (#6563)

sgouezel committed 4 years ago

85c6a799

feat(data/polynomial/*): more lemmas, especially for noncommutative rings (#6599)

kim-em committed 4 years ago

dae047ed

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

leanprover-community-bot committed 4 years ago

b8526489

feat(.docker): Docker containers for debian, alpine, and gitpod (#6515)

kim-em committed 4 years ago

2dabe5af

fix (topology/algebra/basic): fix universe issue with of_nhds_one (#6647)

kbuzzard committed 4 years ago

b1aafb20

eric-wieser committed 4 years ago

391ad51e

Add a missing lemma about alg_equiv conversions

eric-wieser committed 4 years ago

a27742c1

Eliminate a slow convert

eric-wieser committed 4 years ago

e2721ab3

Fill in an "underscore"

eric-wieser committed 4 years ago

38a38990

fill in difficult underscore

eric-wieser committed 4 years ago

0f0b4ebe

feat(data/multiset/basic): Multiset induction lemma (#6623)

tb65536 committed 4 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 4 years ago

bd3695ac

feat(topology/algebra/infinite_sum): add `tsum_even_add_odd` (#6620)

urkud committed 4 years ago

998a3827

refactor(data/{,mv_}polynomial): support function (#6615)

gebner committed 4 years ago

95a8e958

feat(topology/algebra/ordered): generalize `real.compact_Icc` (#6602)

urkud committed 4 years ago

f5c9d0f4

eric-wieser committed 4 years ago

f14ccfb7

refactor(module/submodule): allow submodules to be used for sub-distrib_mul_actions

eric-wieser committed 4 years ago

ee7eedd2

fix(normed_space/multilinear): speed up slow proof (#6639)

robertylewis committed 4 years ago

3b3a8b55

chore(tactic/interactive): propagate tags in `substs` (#6638)

eric-wieser committed 4 years ago

3d451c70

feat(group_theory/subgroup): le_ker_iff (#6630)

tb65536 committed 4 years ago

9beec03c

refactor(data/polynomial/degree/definitions): Remove hypothesis of nat_degree_X_pow_sub_C (#6628)

tb65536 committed 4 years ago

57fda28f

feat(field_theory/polynomial_galois_group): ext lemma (#6627)

tb65536 committed 4 years ago

41f11966

feat(group_theory/solvable): Commutative groups are solvable (#6625)

tb65536 committed 4 years ago

3dd12573

feat(field_theory/splitting_field): splits_pow (#6624)

tb65536 committed 4 years ago

2c4a9855

refactor(topology): make is_closed a class (#6552)

sgouezel committed 4 years ago

653fd292

feat(measure_theory/pi_system) lemmas for pi_system, useful for independence. (#6353)

mzinkevi committed 4 years ago

56065f7e

feat(linear_algebra/basic): add missing lemma finsupp.sum_smul_index_linear_map' (#6565)

ocfnash committed 4 years ago

925ea07d

chore(geometry/manifold): use notation `𝓘(𝕜, E)` (#6636)

urkud committed 4 years ago

b7c5709d

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

leanprover-community-bot committed 4 years ago

514973a9

Newer Older