Commit 2025-11-18 17:49 9d82d224

View on Github →

feat: more API on tsupport and operations on functions (#31549) Variants of Function.mulSupport_one, Function.mulSupport_binop_subset, Function.mulSupport_inv, Function.mulSupport_div... for the topological support.

Estimated changes

Modified Archive/Hairer.lean

Modified Mathlib/Topology/Algebra/Support.lean

added theorem mulTSupport_binop_subset

added theorem mulTSupport_div

added theorem mulTSupport_fun_inv

added theorem mulTSupport_fun_one

added theorem mulTSupport_inv

modified theorem mulTSupport_mul

added theorem mulTSupport_mul_inv

added theorem mulTSupport_one

added theorem mulTSupport_pow

modified theorem tsupport_smul_subset_left

modified theorem tsupport_smul_subset_right