Theorems · Theorem · group theory
Function.support_mul
∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] (f g : ι → M₀),
(Function.support fun x => f x * g x) = Function.support f ∩ Function.support g- Defined in
- Mathlib.Algebra.GroupWithZero.Indicator
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext, Quot.sound
- Assumes
- MulZeroClassNoZeroDivisors
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.extproof · cited by 2,266
- Function.supportstatement and proof · cited by 610
- NoZeroDivisorsstatement and proof · cited by 545
- MulZeroClassstatement and proof · cited by 232
Cited by14
Results whose statement or proof uses this declaration.
- Function.support_divproof · cited by 4
- ExistsContDiffBumpBase.w_supportproof · cited by 4
- MeromorphicOn.circleAverage_log_normproof · cited by 3
- Function.locallyFinsuppWithin.logCounting_monoproof · cited by 2
- circleAverage_log_norm_factorizedRationalproof · cited by 1
- ExistsContDiffBumpBase.y_pos_of_mem_ballproof · cited by 1
- countingFunction_finsum_eq_finsum_addproof · cited by 1
- Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAtproof · cited by 1
- DirichletCharacter.eulerProduct_log_eq_LSeriesproof · cited by 1
- Function.support_mul'proof · cited by 0
- Function.support_mul_of_ne_zero_leftproof · cited by 0
- Function.support_mul_of_ne_zero_rightproof · cited by 0