leanprover-community/mathlib3

Pull Requests Commits

fpvandoorn committed 3 years ago

7f69a4cb

fiber and vector bundle core

fpvandoorn committed 3 years ago

ade12487

hrmacbeth committed 3 years ago

e749eecc

switch smooth vb definition to new style

hrmacbeth committed 3 years ago

bd90ebb7

hrmacbeth committed 3 years ago

4406f753

finish prod construction

hrmacbeth committed 3 years ago

6d9f4b12

missing lemmas about topology of projection

hrmacbeth committed 3 years ago

2c87946f

crop docs (will need to rewrite+reinstate later)

hrmacbeth committed 3 years ago

b1c42f5c

move some material from vector_ to fiber_bundle

hrmacbeth committed 3 years ago

b60e1fcc

try refactor vector/fiber bundles

fpvandoorn committed 3 years ago

9e364dfb

sketch second smooth manifold with corners instance

fpvandoorn committed 3 years ago

6aecd05a

docs and more sorries

hrmacbeth committed 3 years ago

09dcd484

has_groupoid instance

hrmacbeth committed 3 years ago

fae2bbdc

compare definitions

hrmacbeth committed 3 years ago

05190bc1

add vector bundle file

fpvandoorn committed 3 years ago

69e505aa

hrmacbeth committed 3 years ago

ad7714fb

has_groupoid.comp

hrmacbeth committed 3 years ago

2ca7056f

charted_space.comp

hrmacbeth committed 3 years ago

dfbb6738

feat(algebra/squarefree): squarefree gcds of squarefree elements (#16999)

alexjbest committed 3 years ago

ccbe476c

fix(topology/algebra/uniform_mul_action): remove duplicate typeclasses (#17063)

ocfnash committed 3 years ago

98e8d557

feat(ring_theory/hahn_series): Loosen definition of additive valuation (#17057)

khwilson committed 3 years ago

cb8faf79

feat(geometry/manifold/cont_mdiff): add various properties (#16980)

fpvandoorn committed 3 years ago

91b33017

feat(analysis/asymptotics): prove that a function has derivative 0 using asymptotics (#16934)

fpvandoorn committed 3 years ago

8bf24777

feat(number_theory/kummer_dedekind): define conductor and add basic API plus theorem (#16833)

Paul-Lez committed 3 years ago

813725f8

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

Older