Make fun_prop work for finite (multiplicative) support

We define a new predicate HasFiniteMulSupport (and its additivized version) on functions and provide the infrastructure so that fun_prop can prove it for functions that are built from other functions with finite multiplicative support. The relevant API lemmas are provided in Mathlib.Algebra.FiniteSupport.Basic.

def Function.HasFiniteMulSupport {α : Type u_1} {M : Type u_2} [One M] (f : α → M) : Prop

The function f has finite multiplicative support.

Equations

• Function.HasFiniteMulSupport f = (Function.mulSupport f).Finite

def Function.HasFiniteSupport {α : Type u_1} {M : Type u_2} [Zero M] (f : α → M) : Prop

The function f has finite support.

Equations

• Function.HasFiniteSupport f = (Function.support f).Finite

theorem Function.hasFiniteMulSupport_one {α : Type u_1} {M : Type u_2} [One M] : HasFiniteMulSupport fun (x : α) => 1

theorem Function.hasFiniteSupport_zero {α : Type u_1} {M : Type u_2} [Zero M] : HasFiniteSupport fun (x : α) => 0