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

Commit

2 years ago

feat(manifold/{cont_mdiff,algebra/smooth_functions}): restriction as a homomorphism between spaces of smooth functions (#19209) This splits out for separate review the part of #19094 that is blocking the port.

Author

hrmacbeth

Parents

c14c8fcd

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

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