Commit 2025-10-30 17:37 36663085

chore(Analysis/Distribution/ContDiffMapSupportedIn): remove _apply le… (#31094) …mmas about instances #30198 added both a coe_foo and a foo_apply lemma for foo in {zero,add,sub,neg,smul}: remove the apply lemmas again.

• there was no good reason for having both; when in doubt, use coe lemmas
• for simp, the coe lemmas are equally strong (and having both is very unusual at best),
• when rewriting, one can add Pi.zero_apply and friends.