leanprover-community/mathlib3

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into add-mult-struct

gebner committed 4 years ago

1813c570

Fix ring_theory/valuation/basic

gebner committed 4 years ago

af3572f7

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

Merge remote-tracking branch 'origin/master' into add-mult-struct

gebner committed 4 years ago

9dfc8fdb

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

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

feat(data/dfinsupp): add is_scalar_tower and smul_comm_class (#6614)

eric-wieser committed 4 years ago

0e321167

ci(.github/workflows/build.yml): do not install azcopy, change upload logic (#6613)

bryangingechen committed 4 years ago

a814e189

chore(ring_theory/polynomial/basic): remove a use of comap (#6612)

eric-wieser committed 4 years ago

c5c97f27

chore(topology/metric/hausdorff_distance): use `infi`/`supr` (#6611)

urkud committed 4 years ago

590444c4

chore(linear_algebra/quadratic_form): clean up universe collisions, generalize smul lemmas (#6609)

eric-wieser committed 4 years ago

5be9ceae

Older