smooth_functions}): restriction as a homomorphism between spaces of smooth functions
#19209

Closed

[Merged by Bors] - feat(manifold/{cont_mdiff,algebra/smooth_functions}): restriction as a homomorphism between spaces of smooth functions #19209

hrmacbeth wants to merge 1 commit into master from hrmacbeth-cont_mdiff_lemmas

basic diffgeo lemmas

ffd2e506

hrmacbeth added awaiting-review

hrmacbeth added awaiting-CI

hrmacbeth added t-differential-geometry

hrmacbeth added wait-requested-on

github-actions removed awaiting-CI

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~feat(manifold/{cont_mdiff,algebra/smooth_functions}): restriction as a homomorphism between spaces of smooth functions~~ [Merged by Bors] - feat(manifold/{cont_mdiff,algebra/smooth_functions}): restriction as a homomorphism between spaces of smooth functions 2 years ago

bors closed this 2 years ago

bors deleted the hrmacbeth-cont_mdiff_lemmas branch 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge t-differential-geometry wait-requested-on

Milestone

No milestone

mathlib3 [Merged by Bors] - feat(manifold/{cont_mdiff,algebra/smooth_functions}): restriction as a homomorphism between spaces of smooth functions #19209 Closed

[Merged by Bors] - feat(manifold/{cont_mdiff,algebra/smooth_functions}): restriction as a homomorphism between spaces of smooth functions #19209

mathlib3
[Merged by Bors] - feat(manifold/{cont_mdiff,algebra/smooth_functions}): restriction as a homomorphism between spaces of smooth functions
#19209

Closed