α : Type u_1
β : Type ?u.342023
ι : Type ?u.342026
G : Type ?u.342029
M : Type u_2
N : Type ?u.342035
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α → M
h : ¬a ∈ s
hs : Set.Finite (s ∩ mulSupport f)
⊢ Disjoint {a} s

α : Type u_1
β : Type ?u.342023
ι : Type ?u.342026
G : Type ?u.342029
M : Type u_2
N : Type ?u.342035
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α → M
h : ¬a ∈ s
hs : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite ({a} ∩ mulSupport f)
α : Type u_1
β : Type ?u.342023
ι : Type ?u.342026
G : Type ?u.342029
M : Type u_2
N : Type ?u.342035
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α → M
h : ¬a ∈ s
hs : Set.Finite (s ∩ mulSupport f)
⊢ (∏ᶠ (i : α) (_ : i ∈ insert a s), f i) = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i
rw [insert_eq, finprod_mem_union' _ _ hs, finprod_mem_singleton]
no goals
α : Type u_1
β : Type ?u.342023
ι : Type ?u.342026
G : Type ?u.342029
M : Type u_2
N : Type ?u.342035
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α → M
h : ¬a ∈ s
hs : Set.Finite (s ∩ mulSupport f)
⊢ Disjoint {a} s
rwa [disjoint_singleton_left]
no goals
α : Type u_1
β : Type ?u.342023
ι : Type ?u.342026
G : Type ?u.342029
M : Type u_2
N : Type ?u.342035
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α → M
h : ¬a ∈ s
hs : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite ({a} ∩ mulSupport f)
exact (finite_singleton a).inter_of_left _