Theorems · Definition
Function.HasFiniteMulSupport
{α : Type u_1} → {M : Type u_2} → [One M] → (α → M) → PropThe function f has finite multiplicative support.
- Defined in
- Mathlib.Algebra.FiniteSupport.Defs
- Cited by
- 99 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 23 definitions · uses no axioms
- Assumes
- One
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.Finiteproof · cited by 1,814
- Function.mulSupportproof · cited by 240
Cited by104
Results whose statement or proof uses this declaration.
- finprod_eq_prodstatement and proof · cited by 10
- finprod_def'statement and proof · cited by 8
- finprod_mul_distribstatement and proof · cited by 8
- Ideal.hasFiniteMulSupportstatement · cited by 7
- finprod_defstatement and proof · cited by 7
- finprod_eq_prod_of_mulSupport_toFinset_subsetstatement and proof · cited by 6
- MeromorphicAt.finprodproof · cited by 5
- Function.HasFiniteMulSupport.compstatement and proof · cited by 5
- finprod_inductionproof · cited by 5
- finprod_le_finprodstatement and proof · cited by 5
- finprod_of_not_hasFiniteMulSupportstatement and proof · cited by 5
- MonoidHom.map_finprodstatement and proof · cited by 4