Indicator functions and support of a function in groups with zero

theorem Set.indicator_mul {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (s : Set ι) (f g : ι → M₀) : (s.indicator fun (i : ι) => f i * g i) = fun (i : ι) => s.indicator f i * s.indicator g i

theorem Set.indicator_mul_left {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] {i : ι} (s : Set ι) (f g : ι → M₀) : s.indicator (fun (j : ι) => f j * g j) i = s.indicator f i * g i

theorem Set.indicator_mul_right {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] {i : ι} (s : Set ι) (f g : ι → M₀) : s.indicator (fun (j : ι) => f j * g j) i = f i * s.indicator g i

theorem Set.indicator_mul_const {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) : s.indicator (fun (x : ι) => f x * a) i = s.indicator f i * a

theorem Set.indicator_const_mul {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) : s.indicator (fun (x : ι) => a * f x) i = a * s.indicator f i

theorem Set.inter_indicator_mul {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] {s t : Set ι} (f g : ι → M₀) (i : ι) : (s ∩ t).indicator (fun (j : ι) => f j * g j) i = s.indicator f i * t.indicator g i

theorem Set.inter_indicator_one {ι : Type u_1} {M₀ : Type u_4} [MulZeroOneClass M₀] {s t : Set ι} : (s ∩ t).indicator 1 = s.indicator 1 * t.indicator 1

theorem Set.indicator_prod_one {ι : Type u_1} {κ : Type u_2} {M₀ : Type u_4} [MulZeroOneClass M₀] {s : Set ι} {i : ι} {t : Set κ} {j : κ} : (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j

theorem Set.indicator_eq_zero_iff_notMem {ι : Type u_1} (M₀ : Type u_4) [MulZeroOneClass M₀] {s : Set ι} {i : ι} [Nontrivial M₀] : s.indicator 1 i = 0 ↔ ¬i ∈ s

theorem Set.indicator_eq_one_iff_mem {ι : Type u_1} (M₀ : Type u_4) [MulZeroOneClass M₀] {s : Set ι} {i : ι} [Nontrivial M₀] : s.indicator 1 i = 1 ↔ i ∈ s

theorem Set.indicator_one_inj {ι : Type u_1} (M₀ : Type u_4) [MulZeroOneClass M₀] {s t : Set ι} [Nontrivial M₀] (h : s.indicator 1 = t.indicator 1) : s = t

@[simp]

theorem Function.support_one {ι : Type u_1} (R : Type u_5) [Zero R] [One R] [NeZero 1] : support 1 = Set.univ

@[simp]

theorem Function.mulSupport_zero {ι : Type u_1} (R : Type u_5) [Zero R] [One R] [NeZero 1] : mulSupport 0 = Set.univ

theorem Function.support_mul_subset_left {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (f g : ι → M₀) : (support fun (x : ι) => f x * g x) ⊆ support f

theorem Function.support_mul_subset_right {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (f g : ι → M₀) : (support fun (x : ι) => f x * g x) ⊆ support g

@[simp]

theorem Function.support_mul {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] (f g : ι → M₀) : (support fun (x : ι) => f x * g x) = support f ∩ support g

@[simp]

theorem Function.support_mul' {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] (f g : ι → M₀) : support (f * g) = support f ∩ support g

theorem Function.support_mul_of_ne_zero_left {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] {f : ι → M₀} (hf : ∀ (x : ι), f x ≠ 0) (g : ι → M₀) : (support fun (x : ι) => f x * g x) = support g

If f is everywhere nonzero, then support (f * g) = support g.

theorem Function.support_mul_of_ne_zero_right {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] (f : ι → M₀) {g : ι → M₀} (hg : ∀ (x : ι), g x ≠ 0) : (support fun (x : ι) => f x * g x) = support f

If g is everywhere nonzero, then support (f * g) = support f.

@[simp]

theorem Function.support_pow {ι : Type u_1} {M₀ : Type u_4} [MonoidWithZero M₀] [IsReduced M₀] {n : ℕ} (f : ι → M₀) (hn : n ≠ 0) : (support fun (a : ι) => f a ^ n) = support f

@[simp]

theorem Function.support_pow' {ι : Type u_1} {M₀ : Type u_4} [MonoidWithZero M₀] [IsReduced M₀] {n : ℕ} (f : ι → M₀) (hn : n ≠ 0) : support (f ^ n) = support f

@[simp]

theorem Function.support_inv {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f : ι → G₀) : (support fun (a : ι) => (f a)⁻¹) = support f

@[simp]

theorem Function.support_inv' {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f : ι → G₀) : support f⁻¹ = support f

@[simp]

theorem Function.support_div {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f g : ι → G₀) : (support fun (a : ι) => f a / g a) = support f ∩ support g

@[simp]

theorem Function.support_div' {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f g : ι → G₀) : support (f / g) = support f ∩ support g

theorem Function.mulSupport_one_add {ι : Type u_1} {R : Type u_5} [One R] [AddLeftCancelMonoid R] (f : ι → R) : (mulSupport fun (x : ι) => 1 + f x) = support f

theorem Function.mulSupport_one_add' {ι : Type u_1} {R : Type u_5} [One R] [AddLeftCancelMonoid R] (f : ι → R) : mulSupport (1 + f) = support f

theorem Function.mulSupport_add_one {ι : Type u_1} {R : Type u_5} [One R] [AddRightCancelMonoid R] (f : ι → R) : (mulSupport fun (x : ι) => f x + 1) = support f

theorem Function.mulSupport_add_one' {ι : Type u_1} {R : Type u_5} [One R] [AddRightCancelMonoid R] (f : ι → R) : mulSupport (f + 1) = support f

theorem Function.mulSupport_one_sub' {ι : Type u_1} {R : Type u_5} [One R] [AddGroup R] (f : ι → R) : mulSupport (1 - f) = support f

theorem Function.mulSupport_one_sub {ι : Type u_1} {R : Type u_5} [One R] [AddGroup R] (f : ι → R) : (mulSupport fun (x : ι) => 1 - f x) = support f