Commit 2026-06-10 10:42 b62517f5

View on Github →

feat(Analysis/Distribution): use Is*Apply for SchwartzMap (#40447) We simplify a few proofs and remove a duplicate lemma.

Estimated changes

deleted theorem SchwartzMap.add_apply
deleted theorem SchwartzMap.coeFn_zero
deleted def SchwartzMap.coeHom
deleted theorem SchwartzMap.coe_coeHom
deleted theorem SchwartzMap.coe_zero
deleted theorem SchwartzMap.neg_apply
deleted theorem SchwartzMap.smul_apply
deleted theorem SchwartzMap.sub_apply
deleted theorem SchwartzMap.sum_apply
deleted theorem SchwartzMap.zero_apply