Commit 2024-01-16 22:20 d602bc27

refactor(ContMDiff/Basic): multiplicativise, generalise and golf contMDiff_of_support and friends (#9764)

• multiplicativise contMDiff_of_support, contMDiffWithinAt_of_not_mem and contMDiffAt_of_not_mem and use to_additive
• golf extend_one with the multiplicative version
• generalise these lemmas to manifolds with zero/one
• slight clean-up: remove unused variables and opens
• slight drive-by golfing of one proof
• deprecate eventuallyEq_zero_nhds in favor of not_mem_tsupport_iff_eventuallyEq Addresses the post-merge review comments in #9669.