leanprover-community/mathlib

Pull Requests Commits

EdAyers committed 5 years ago

1c59024f

Initial list/zipper.lean

EdAyers committed 5 years ago

5bf62d60

chore(topology/algebra/infinite_sum): speedup has_sum_sum (#5710)

jcommelin committed 5 years ago

10259082

feat(submonoid/basic): subsingleton and nontrivial instances for {add_,}submonoid (#5690)

eric-wieser committed 5 years ago

73ba4602

docs(undergrad.yaml): analysis updates (#5675)

hrmacbeth committed 5 years ago

e76fdb9e

feat(linear_algebra/multilinear_map): Add `range` and `map` (#5658)

eric-wieser committed 5 years ago

ce6a7eba

feat(measure_theory): each set has a measurable superset of the same measure (#5688)

urkud committed 5 years ago

3a3ec6c3

feat(data/set/intervals): add 2 Icc ssubset lemmas (#5617)

Mohamed Al-Fahim committed 5 years ago

26710686

chore(category_theory/limits): move constructions folder (#5681)

b-mehta committed 5 years ago

cd7a8a18

fix(linear_algebra/tensor_product): Remove the priorities from the module structure (#5667)

eric-wieser committed 5 years ago

be75005c

chore(category_theory/limits/over): generalise, golf and document over limits (#5674)

b-mehta committed 5 years ago

cd0d8c02

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

leanprover-community-bot committed 5 years ago

9f9f85e8

feat(measure_theory/pi): `ae_eq` lemmas about intervals in `Π i, α i` (#5633)

urkud committed 5 years ago

049f16a8

feat(algebra/splitting_field): Restrict to splitting field (#5562)

tb65536 committed 5 years ago

b537cc08

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

leanprover-community-bot committed 5 years ago

c112ad03

feat(analysis/special/functions/trigonometric): complex trig and some even/odd lemmas (#5404)

benjamindavidson committed 5 years ago

08800bb7

feat(equiv|set|topology): various additions (#5656)

fpvandoorn committed 5 years ago

cc6f039f

chore(measure_theory/set_integral): use weaker assumptions here and there (#5647)

urkud committed 5 years ago

62c1912e

feat(field_theory/separable): Remove hypothesis in irreducible.separable (#5687)

tb65536 committed 5 years ago

3e7efd4e

feat(order/complete_well_founded): characterise well-foundedness for complete lattices (#5575)

Oliver Nash committed 5 years ago

b72811f2

chore(order/filter): a few more lemmas about `eventually` and set operations (#5686)

urkud committed 5 years ago

0d9cb85e

chore(order/filter/basic): a few `simp` lemmas (#5685)

urkud committed 5 years ago

b0c35d12

feat(data/equiv/basic, logic/embedding): swap commutes with injective functions (#5636)

pechersky committed 5 years ago

1c4f2aec

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

leanprover-community-bot committed 5 years ago

a28602a7

feat(algebra/lie/basic): Lie ideal operations are linear spans (#5676)

Oliver Nash committed 5 years ago

f60c184e

feat(measure_theory/lp_space): add more lemmas about snorm (#5644)

RemyDegenne committed 5 years ago

5faf34cc

chore(data/set/lattice): add a few simp lemmas (#5671)

urkud committed 5 years ago

fdec90ad

feat(topology/separation, topology/metric_space/basic): add lemmas on discrete subsets of a topological space (#5523)

adomani committed 5 years ago

3166f4ef

feat(topology/algebra/ordered): prove `tendsto.Icc` for pi-types (#5639)

urkud committed 5 years ago

a161256c

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

leanprover-community-bot committed 5 years ago

faf1a983

Older