Documentation

Mathlib.Algebra.GroupWithZero.Indicator

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 : ιM₀) (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 : ιM₀) (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 : ιM₀) (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 : Set ι} {t : Set ι} (f : ιM₀) (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 : Set ι} {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_not_mem {ι : Type u_1} (M₀ : Type u_4) [MulZeroOneClass M₀] {s : Set ι} {i : ι} [Nontrivial M₀] :
s.indicator 1 i = 0 is
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 : Set ι} {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] :
Function.support 1 = Set.univ
@[simp]
theorem Function.mulSupport_zero {ι : Type u_1} (R : Type u_5) [Zero R] [One R] [NeZero 1] :
theorem Function.support_mul_subset_left {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (f : ιM₀) (g : ιM₀) :
(Function.support fun (x : ι) => f x * g x) Function.support f
theorem Function.support_mul_subset_right {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] (f : ιM₀) (g : ιM₀) :
(Function.support fun (x : ι) => f x * g x) Function.support g
@[simp]
theorem Function.support_mul {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] (f : ιM₀) (g : ιM₀) :
@[simp]
theorem Function.support_mul' {ι : Type u_1} {M₀ : Type u_4} [MulZeroClass M₀] [NoZeroDivisors M₀] (f : ιM₀) (g : ιM₀) :
@[simp]
theorem Function.support_pow {ι : Type u_1} {M₀ : Type u_4} [MonoidWithZero M₀] [NoZeroDivisors M₀] {n : } (f : ιM₀) (hn : n 0) :
(Function.support fun (a : ι) => f a ^ n) = Function.support f
@[simp]
theorem Function.support_pow' {ι : Type u_1} {M₀ : Type u_4} [MonoidWithZero M₀] [NoZeroDivisors M₀] {n : } (f : ιM₀) (hn : n 0) :
@[simp]
theorem Function.support_inv {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f : ιG₀) :
(Function.support fun (a : ι) => (f a)⁻¹) = Function.support f
@[simp]
theorem Function.support_inv' {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f : ιG₀) :
@[simp]
theorem Function.support_div {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f : ιG₀) (g : ιG₀) :
@[simp]
theorem Function.support_div' {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] (f : ιG₀) (g : ιG₀) :
theorem Function.mulSupport_one_add {ι : Type u_1} {R : Type u_5} [One R] [AddLeftCancelMonoid R] (f : ιR) :
(Function.mulSupport fun (x : ι) => 1 + f x) = Function.support f
theorem Function.mulSupport_one_add' {ι : Type u_1} {R : Type u_5} [One R] [AddLeftCancelMonoid R] (f : ιR) :
theorem Function.mulSupport_add_one {ι : Type u_1} {R : Type u_5} [One R] [AddRightCancelMonoid R] (f : ιR) :
(Function.mulSupport fun (x : ι) => f x + 1) = Function.support f
theorem Function.mulSupport_add_one' {ι : Type u_1} {R : Type u_5} [One R] [AddRightCancelMonoid R] (f : ιR) :
theorem Function.mulSupport_one_sub' {ι : Type u_1} {R : Type u_5} [One R] [AddGroup R] (f : ιR) :
theorem Function.mulSupport_one_sub {ι : Type u_1} {R : Type u_5} [One R] [AddGroup R] (f : ιR) :
(Function.mulSupport fun (x : ι) => 1 - f x) = Function.support f