leanprover-community/mathlib

Pull Requests Commits

more cleanup/docsctrings

CBirkbeck committed 3 years ago

5bb5dc98

still some doc strings missing

CBirkbeck committed 3 years ago

4a9a3c5e

CBirkbeck committed 3 years ago

5d9099b9

CBirkbeck committed 3 years ago

ab0f82ef

pre-golf merge fix

CBirkbeck committed 3 years ago

1f94979c

CBirkbeck committed 3 years ago

8bd703b7

Merge branch 'circle_transform_pt2' of https://github.com/leanprover-community/mathlib into circle_transform_pt2

CBirkbeck committed 3 years ago

e19a6e50

CBirkbeck committed 3 years ago

a013356e

CBirkbeck committed 3 years ago

6fa8e7d5

CBirkbeck committed 3 years ago

ae2a9b68

chore(probability/independence): simplify the definition of pi_Union_Inter (#17043)

RemyDegenne committed 3 years ago

0b045c73

refactor(data/finsupp/ne_locus): Match `dist` API (#17036)

YaelDillies committed 3 years ago

22e33e9d

feat(data/multiset/interval): locally finite order on multisets (#17028)

eric-wieser committed 3 years ago

056a7a1a

feat(algebraic_geometry/prime_spectrum/noetherian): The spectrum of a noetherian ring is noetherian. (#17016)

erdOne committed 3 years ago

689184f7

feat(topology/algebra/uniform_convergence): criterion for a vector subspace of `α → E` to be a TVS for the topology of 𝔖-convergence (#14857)

ADedecker committed 3 years ago

f01de4e1

chore(algebra/module/basic): reduce imports (#17042)

kim-em committed 3 years ago

edfb391a

chore(logic/equiv/basic): split into two files (#17038)

kim-em committed 3 years ago

9407b033

fix(data/set/basic): Fix `set.lt_iff_ssubset`. (#17047)

erdOne committed 3 years ago

8c9b0057

feat(order/upper_lower): Maps of upper sets (#17007)

YaelDillies committed 3 years ago

4af7699b

fix(topology/metric_space/gromov_hausdorff): squeeze all simps (#17049)

fpvandoorn committed 3 years ago

3d197c69

feat(measure_theory/measure): `measure_Union_null_iff` for Props (#17029)

alexjbest committed 3 years ago

0b480ff9

chore(order/lattice): add lemmas about `sup` and `inf` on `prod` (#17040)

eric-wieser committed 3 years ago

3812c1ce

feat(scripts/port_status): script to show currently portable files (#17009)

kim-em committed 3 years ago

6d4f6107

feat(*): add various order-related lemmas (#16918)

ocfnash committed 3 years ago

a5347cb9

feat(analysis/calculus/cont_diff): strengthen lemma (#16933)

fpvandoorn committed 3 years ago

38992f94

feat(combinatorics/simple_graph/regularity/bound): `positivity` extension (#16639)

YaelDillies committed 3 years ago

8f774b71

feat(data/polynomial): a couple of lemmas on nat degree and roots of maps (#16992)

alexjbest committed 3 years ago

d8dd620c

feat(ring_theory/finiteness): A morphism is finitely presented if the composition with a finite morphism is. (#15949)

erdOne committed 3 years ago

cf94743b

feat(topology/subset_properties, noetherian_space): Noetherian spaces have finite irreducible components. (#17015)

erdOne committed 3 years ago

6d94ff7b

refactor(geometry/manifold/cont_mdiff): split everything about mfderiv (#16982)

fpvandoorn committed 3 years ago

2b69cd5e

Older