Type of functions with finite support
For any type α and a type β with zero, we define the type finsupp α β of finitely supported
functions from α to β, i.e. the functions which are zero everywhere on α except on a finite
set. We write this in infix notation as α →₀ β.
Functions with finite support provide the basis for the following concrete instances:
ℕ →₀ α: Polynomials (whereαis a ring)(σ →₀ ℕ) →₀ α: Multivariate Polynomials (againαis a ring, andσare variable names)α →₀ ℕ: Multisetsα →₀ ℤ: Abelian groups freely generated byαβ →₀ α: Linear combinations overβwhereαis the scalar ring
Most of the theory assumes that the range is a commutative monoid. This gives us the big sum
operator as a powerful way to construct finsupp elements.
A general piece of advice is to not use α →₀ β directly, as the type class setup might not be a
good fit. Defining a copy and selecting the instances that are best suited for the application works
better.
Implementation notes
This file is a noncomputable theory and uses classical logic throughout.
Notation
This file defines α →₀ β as notation for finsupp α β.
finsupp α β, denoted α →₀ β, is the type of functions f : α → β such that
f x = 0 for all but finitely many x.
Basic declarations about finsupp
@[instance]
Equations
- finsupp.has_coe_to_fun = {F := λ (_x : α →₀ β), α → β, coe := finsupp.to_fun _inst_1}
@[instance]
Equations
- finsupp.has_zero = {zero := {support := ∅, to_fun := λ (_x : α), 0, mem_support_to_fun := _}}
@[simp]
@[instance]
Equations
- finsupp.inhabited = {default := 0}
@[instance]
def
finsupp.finsupp.decidable_eq
{α : Type u_1}
{β : Type u_2}
[has_zero β]
[decidable_eq α]
[decidable_eq β] :
decidable_eq (α →₀ β)
Given fintype α, equiv_fun_on_fintype is the equiv between α →₀ β and α → β.
(All functions on a finite type are finitely supported.)
Equations
- finsupp.equiv_fun_on_fintype = {to_fun := λ (f : α →₀ β) (a : α), ⇑f a, inv_fun := λ (f : α → β), {support := finset.filter (λ (a : α), f a ≠ 0) finset.univ, to_fun := f, mem_support_to_fun := _}, left_inv := _, right_inv := _}
Declarations about single
single a b is the finitely supported function which has
value b at a and zero otherwise.
theorem
finsupp.single_apply
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a a' : α}
{b : β} :
⇑(finsupp.single a b) a' = ite (a = a') b 0
@[simp]
theorem
finsupp.single_eq_same
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a : α}
{b : β} :
⇑(finsupp.single a b) a = b
@[simp]
theorem
finsupp.single_eq_of_ne
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a a' : α}
{b : β}
(h : a ≠ a') :
⇑(finsupp.single a b) a' = 0
@[simp]
theorem
finsupp.single_zero
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a : α} :
finsupp.single a 0 = 0
theorem
finsupp.support_single_ne_zero
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a : α}
{b : β}
(hb : b ≠ 0) :
(finsupp.single a b).support = {a}
theorem
finsupp.support_single_subset
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a : α}
{b : β} :
(finsupp.single a b).support ⊆ {a}
theorem
finsupp.single_eq_single_iff
{α : Type u_1}
{β : Type u_2}
[has_zero β]
(a₁ a₂ : α)
(b₁ b₂ : β) :
theorem
finsupp.single_left_inj
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a a' : α}
{b : β}
(h : b ≠ 0) :
finsupp.single a b = finsupp.single a' b ↔ a = a'
theorem
finsupp.single_eq_zero
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a : α}
{b : β} :
finsupp.single a b = 0 ↔ b = 0
theorem
finsupp.single_swap
{α : Type u_1}
{β : Type u_2}
[has_zero β]
(a₁ a₂ : α)
(b : β) :
⇑(finsupp.single a₁ b) a₂ = ⇑(finsupp.single a₂ b) a₁
theorem
finsupp.unique_single
{α : Type u_1}
{β : Type u_2}
[has_zero β]
[unique α]
(x : α →₀ β) :
x = finsupp.single (default α) (⇑x (default α))
@[simp]
theorem
finsupp.unique_single_eq_iff
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a a' : α}
{b : β}
[unique α]
{b' : β} :
finsupp.single a b = finsupp.single a' b' ↔ b = b'
Declarations about on_finset
def
finsupp.on_finset
{α : Type u_1}
{β : Type u_2}
[has_zero β]
(s : finset α)
(f : α → β)
(hf : ∀ (a : α), f a ≠ 0 → a ∈ s) :
α →₀ β
on_finset s f hf is the finsupp function representing f restricted to the finset s.
The function needs to be 0 outside of s. Use this when the set needs to be filtered anyways,
otherwise a better set representation is often available.
Equations
- finsupp.on_finset s f hf = {support := finset.filter (λ (a : α), f a ≠ 0) s, to_fun := f, mem_support_to_fun := _}
@[simp]
theorem
finsupp.on_finset_apply
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{s : finset α}
{f : α → β}
{hf : ∀ (a : α), f a ≠ 0 → a ∈ s}
{a : α} :
⇑(finsupp.on_finset s f hf) a = f a
@[simp]
theorem
finsupp.support_on_finset_subset
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{s : finset α}
{f : α → β}
{hf : ∀ (a : α), f a ≠ 0 → a ∈ s} :
(finsupp.on_finset s f hf).support ⊆ s
theorem
finsupp.support_on_finset
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{s : finset α}
{f : α → β}
(hf : ∀ (a : α), f a ≠ 0 → a ∈ s) :
(finsupp.on_finset s f hf).support = finset.filter (λ (a : α), f a ≠ 0) s
Declarations about map_range
def
finsupp.map_range
{α : Type u_1}
{β₁ : Type u_8}
{β₂ : Type u_9}
[has_zero β₁]
[has_zero β₂]
(f : β₁ → β₂)
(hf : f 0 = 0)
(g : α →₀ β₁) :
α →₀ β₂
The composition of f : β₁ → β₂ and g : α →₀ β₁ is
map_range f hf g : α →₀ β₂, well-defined when f 0 = 0.
Equations
- finsupp.map_range f hf g = finsupp.on_finset g.support (f ∘ ⇑g) _
@[simp]
theorem
finsupp.map_range_apply
{α : Type u_1}
{β₁ : Type u_8}
{β₂ : Type u_9}
[has_zero β₁]
[has_zero β₂]
{f : β₁ → β₂}
{hf : f 0 = 0}
{g : α →₀ β₁}
{a : α} :
⇑(finsupp.map_range f hf g) a = f (⇑g a)
@[simp]
theorem
finsupp.map_range_zero
{α : Type u_1}
{β₁ : Type u_8}
{β₂ : Type u_9}
[has_zero β₁]
[has_zero β₂]
{f : β₁ → β₂}
{hf : f 0 = 0} :
finsupp.map_range f hf 0 = 0
theorem
finsupp.support_map_range
{α : Type u_1}
{β₁ : Type u_8}
{β₂ : Type u_9}
[has_zero β₁]
[has_zero β₂]
{f : β₁ → β₂}
{hf : f 0 = 0}
{g : α →₀ β₁} :
(finsupp.map_range f hf g).support ⊆ g.support
@[simp]
theorem
finsupp.map_range_single
{α : Type u_1}
{β₁ : Type u_8}
{β₂ : Type u_9}
[has_zero β₁]
[has_zero β₂]
{f : β₁ → β₂}
{hf : f 0 = 0}
{a : α}
{b : β₁} :
finsupp.map_range f hf (finsupp.single a b) = finsupp.single a (f b)
Declarations about emb_domain
def
finsupp.emb_domain
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[has_zero β]
(f : α₁ ↪ α₂)
(v : α₁ →₀ β) :
α₂ →₀ β
Given f : α₁ ↪ α₂ and v : α₁ →₀ β, emb_domain f v : α₂ →₀ β
is the finitely supported function whose value at f a : α₂ is v a.
For a b : α₂ outside the range of f, it is zero.
Equations
- finsupp.emb_domain f v = {support := finset.map f v.support, to_fun := λ (a₂ : α₂), dite (a₂ ∈ finset.map f v.support) (λ (h : a₂ ∈ finset.map f v.support), ⇑v (finset.choose (λ (a₁ : α₁), ⇑f a₁ = a₂) v.support _)) (λ (h : a₂ ∉ finset.map f v.support), 0), mem_support_to_fun := _}
theorem
finsupp.support_emb_domain
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[has_zero β]
(f : α₁ ↪ α₂)
(v : α₁ →₀ β) :
(finsupp.emb_domain f v).support = finset.map f v.support
theorem
finsupp.emb_domain_zero
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[has_zero β]
(f : α₁ ↪ α₂) :
finsupp.emb_domain f 0 = 0
theorem
finsupp.emb_domain_apply
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[has_zero β]
(f : α₁ ↪ α₂)
(v : α₁ →₀ β)
(a : α₁) :
⇑(finsupp.emb_domain f v) (⇑f a) = ⇑v a
theorem
finsupp.emb_domain_inj
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[has_zero β]
{f : α₁ ↪ α₂}
{l₁ l₂ : α₁ →₀ β} :
finsupp.emb_domain f l₁ = finsupp.emb_domain f l₂ ↔ l₁ = l₂
theorem
finsupp.emb_domain_map_range
{α₁ : Type u_6}
{α₂ : Type u_7}
{β₁ : Type u_1}
{β₂ : Type u_2}
[has_zero β₁]
[has_zero β₂]
(f : α₁ ↪ α₂)
(g : β₁ → β₂)
(p : α₁ →₀ β₁)
(hg : g 0 = 0) :
finsupp.emb_domain f (finsupp.map_range g hg p) = finsupp.map_range g hg (finsupp.emb_domain f p)
theorem
finsupp.single_of_emb_domain_single
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[has_zero β]
(l : α₁ →₀ β)
(f : α₁ ↪ α₂)
(a : α₂)
(b : β)
(hb : b ≠ 0)
(h : finsupp.emb_domain f l = finsupp.single a b) :
∃ (x : α₁), l = finsupp.single x b ∧ ⇑f x = a
Declarations about zip_with
def
finsupp.zip_with
{α : Type u_1}
{β : Type u_2}
{β₁ : Type u_8}
{β₂ : Type u_9}
[has_zero β]
[has_zero β₁]
[has_zero β₂]
(f : β₁ → β₂ → β)
(hf : f 0 0 = 0)
(g₁ : α →₀ β₁)
(g₂ : α →₀ β₂) :
α →₀ β
zip_with f hf g₁ g₂ is the finitely supported function satisfying
zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a), and it is well-defined when f 0 0 = 0.
Equations
- finsupp.zip_with f hf g₁ g₂ = finsupp.on_finset (g₁.support ∪ g₂.support) (λ (a : α), f (⇑g₁ a) (⇑g₂ a)) _
Declarations about erase
erase a f is the finitely supported function equal to f except at a where it is equal to
0.
@[simp]
theorem
finsupp.support_erase
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a : α}
{f : α →₀ β} :
(finsupp.erase a f).support = f.support.erase a
@[simp]
theorem
finsupp.erase_same
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a : α}
{f : α →₀ β} :
⇑(finsupp.erase a f) a = 0
@[simp]
theorem
finsupp.erase_ne
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a a' : α}
{f : α →₀ β}
(h : a' ≠ a) :
⇑(finsupp.erase a f) a' = ⇑f a'
@[simp]
theorem
finsupp.erase_single
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a : α}
{b : β} :
finsupp.erase a (finsupp.single a b) = 0
theorem
finsupp.erase_single_ne
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{a a' : α}
{b : β}
(h : a ≠ a') :
finsupp.erase a (finsupp.single a' b) = finsupp.single a' b
Declarations about sum and prod
In most of this section, the domain β is assumed to be an add_monoid.
def
finsupp.sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_zero β]
[add_comm_monoid γ]
(f : α →₀ β)
(g : α → β → γ) :
γ
sum f g is the sum of g a (f a) over the support of f.
def
finsupp.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_zero β]
[comm_monoid γ]
(f : α →₀ β)
(g : α → β → γ) :
γ
prod f g is the product of g a (f a) over the support of f.
theorem
finsupp.prod_fintype
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[fintype α]
[has_zero β]
[comm_monoid γ]
(f : α →₀ β)
(g : α → β → γ)
(h : ∀ (i : α), g i 0 = 1) :
theorem
finsupp.sum_fintype
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[fintype α]
[has_zero β]
[add_comm_monoid γ]
(f : α →₀ β)
(g : α → β → γ)
(h : ∀ (i : α), g i 0 = 0) :
theorem
finsupp.sum_map_range_index
{α : Type u_1}
{γ : Type u_3}
{β₁ : Type u_8}
{β₂ : Type u_9}
[has_zero β₁]
[has_zero β₂]
[add_comm_monoid γ]
{f : β₁ → β₂}
{hf : f 0 = 0}
{g : α →₀ β₁}
{h : α → β₂ → γ}
(h0 : ∀ (a : α), h a 0 = 0) :
(finsupp.map_range f hf g).sum h = g.sum (λ (a : α) (b : β₁), h a (f b))
theorem
finsupp.prod_map_range_index
{α : Type u_1}
{γ : Type u_3}
{β₁ : Type u_8}
{β₂ : Type u_9}
[has_zero β₁]
[has_zero β₂]
[comm_monoid γ]
{f : β₁ → β₂}
{hf : f 0 = 0}
{g : α →₀ β₁}
{h : α → β₂ → γ}
(h0 : ∀ (a : α), h a 0 = 1) :
(finsupp.map_range f hf g).prod h = g.prod (λ (a : α) (b : β₁), h a (f b))
theorem
finsupp.prod_zero_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
[comm_monoid γ]
{h : α → β → γ} :
theorem
finsupp.sum_zero_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
[add_comm_monoid γ]
{h : α → β → γ} :
theorem
finsupp.prod_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{α' : Type u_4}
[has_zero β]
{β' : Type u_5}
[has_zero β']
(f : α →₀ β)
(g : α' →₀ β')
[comm_monoid γ]
(h : α → β → α' → β' → γ) :
theorem
finsupp.sum_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{α' : Type u_4}
[has_zero β]
{β' : Type u_5}
[has_zero β']
(f : α →₀ β)
(g : α' →₀ β')
[add_comm_monoid γ]
(h : α → β → α' → β' → γ) :
@[simp]
theorem
finsupp.prod_ite_eq'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_zero β]
[comm_monoid γ]
(f : α →₀ β)
(a : α)
(b : α → β → γ) :
A restatement of prod_ite_eq with the equality test reversed.
@[simp]
theorem
finsupp.sum_ite_eq'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_zero β]
[add_comm_monoid γ]
(f : α →₀ β)
(a : α)
(b : α → β → γ) :
A restatement of sum_ite_eq with the equality test reversed.
theorem
finsupp.on_finset_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_zero β]
[add_comm_monoid γ]
{s : finset α}
{f : α → β}
{g : α → β → γ}
(hf : ∀ (a : α), f a ≠ 0 → a ∈ s)
(hg : ∀ (a : α), g a 0 = 0) :
(finsupp.on_finset s f hf).sum g = ∑ (a : α) in s, g a (f a)
If g maps a second argument of 0 to 0, summing it over the
result of on_finset is the same as summing it over the original
finset.
theorem
finsupp.prod_single_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_monoid β]
[comm_monoid γ]
{a : α}
{b : β}
{h : α → β → γ}
(h_zero : h a 0 = 1) :
(finsupp.single a b).prod h = h a b
theorem
finsupp.sum_single_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_monoid β]
[add_comm_monoid γ]
{a : α}
{b : β}
{h : α → β → γ}
(h_zero : h a 0 = 0) :
(finsupp.single a b).sum h = h a b
@[instance]
Equations
- finsupp.has_add = {add := finsupp.zip_with has_add.add finsupp.has_add._proof_1}
@[simp]
@[simp]
theorem
finsupp.single_add
{α : Type u_1}
{β : Type u_2}
[add_monoid β]
{a : α}
{b₁ b₂ : β} :
finsupp.single a (b₁ + b₂) = finsupp.single a b₁ + finsupp.single a b₂
@[instance]
Equations
- finsupp.add_monoid = {add := has_add.add finsupp.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _}
Evaluation of a function f : α →₀ β at a point as an additive monoid homomorphism.
@[simp]
theorem
finsupp.eval_add_hom_apply
{α : Type u_1}
{β : Type u_2}
[add_monoid β]
(a : α)
(g : α →₀ β) :
⇑(finsupp.eval_add_hom a) g = ⇑g a
theorem
finsupp.single_add_erase
{α : Type u_1}
{β : Type u_2}
[add_monoid β]
{a : α}
{f : α →₀ β} :
finsupp.single a (⇑f a) + finsupp.erase a f = f
theorem
finsupp.erase_add_single
{α : Type u_1}
{β : Type u_2}
[add_monoid β]
{a : α}
{f : α →₀ β} :
finsupp.erase a f + finsupp.single a (⇑f a) = f
@[simp]
theorem
finsupp.erase_add
{α : Type u_1}
{β : Type u_2}
[add_monoid β]
(a : α)
(f f' : α →₀ β) :
finsupp.erase a (f + f') = finsupp.erase a f + finsupp.erase a f'
theorem
finsupp.induction
{α : Type u_1}
{β : Type u_2}
[add_monoid β]
{p : (α →₀ β) → Prop}
(f : α →₀ β)
(h0 : p 0)
(ha : ∀ (a : α) (b : β) (f : α →₀ β), a ∉ f.support → b ≠ 0 → p f → p (finsupp.single a b + f)) :
p f
theorem
finsupp.induction₂
{α : Type u_1}
{β : Type u_2}
[add_monoid β]
{p : (α →₀ β) → Prop}
(f : α →₀ β)
(h0 : p 0)
(ha : ∀ (a : α) (b : β) (f : α →₀ β), a ∉ f.support → b ≠ 0 → p f → p (f + finsupp.single a b)) :
p f
theorem
finsupp.map_range_add
{α : Type u_1}
{β₁ : Type u_8}
{β₂ : Type u_9}
[add_monoid β₁]
[add_monoid β₂]
{f : β₁ → β₂}
{hf : f 0 = 0}
(hf' : ∀ (x y : β₁), f (x + y) = f x + f y)
(v₁ v₂ : α →₀ β₁) :
finsupp.map_range f hf (v₁ + v₂) = finsupp.map_range f hf v₁ + finsupp.map_range f hf v₂
@[instance]
Equations
- finsupp.nat_sub = {sub := finsupp.zip_with (λ (m n : ℕ), m - n) finsupp.nat_sub._proof_1}
@[simp]
theorem
finsupp.single_sub
{α : Type u_1}
{a : α}
{n₁ n₂ : ℕ} :
finsupp.single a (n₁ - n₂) = finsupp.single a n₁ - finsupp.single a n₂
theorem
finsupp.sub_single_one_add
{α : Type u_1}
{a : α}
{u u' : α →₀ ℕ}
(h : ⇑u a ≠ 0) :
u - finsupp.single a 1 + u' = u + u' - finsupp.single a 1
theorem
finsupp.add_sub_single_one
{α : Type u_1}
{a : α}
{u u' : α →₀ ℕ}
(h : ⇑u' a ≠ 0) :
u + (u' - finsupp.single a 1) = u + u' - finsupp.single a 1
@[instance]
def
finsupp.add_comm_monoid
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid β] :
add_comm_monoid (α →₀ β)
Equations
- finsupp.add_comm_monoid = {add := add_monoid.add finsupp.add_monoid, add_assoc := _, zero := add_monoid.zero finsupp.add_monoid, zero_add := _, add_zero := _, add_comm := _}
@[instance]
Equations
- finsupp.add_group = {add := add_monoid.add finsupp.add_monoid, add_assoc := _, zero := add_monoid.zero finsupp.add_monoid, zero_add := _, add_zero := _, neg := finsupp.map_range has_neg.neg neg_zero, add_left_neg := _}
theorem
finsupp.single_multiset_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid β]
(s : multiset β)
(a : α) :
finsupp.single a s.sum = (multiset.map (finsupp.single a) s).sum
theorem
finsupp.single_finset_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
(s : finset γ)
(f : γ → β)
(a : α) :
finsupp.single a (∑ (b : γ) in s, f b) = ∑ (b : γ) in s, finsupp.single a (f b)
theorem
finsupp.single_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[has_zero γ]
[add_comm_monoid β]
(s : δ →₀ γ)
(f : δ → γ → β)
(a : α) :
finsupp.single a (s.sum f) = s.sum (λ (d : δ) (c : γ), finsupp.single a (f d c))
@[instance]
def
finsupp.add_comm_group
{α : Type u_1}
{β : Type u_2}
[add_comm_group β] :
add_comm_group (α →₀ β)
Equations
- finsupp.add_comm_group = {add := add_group.add finsupp.add_group, add_assoc := _, zero := add_group.zero finsupp.add_group, zero_add := _, add_zero := _, neg := add_group.neg finsupp.add_group, add_left_neg := _, add_comm := _}
@[simp]
theorem
finsupp.sum_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
[add_comm_monoid γ]
{f : α →₀ β} :
@[simp]
theorem
finsupp.sum_add
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
[add_comm_monoid γ]
{f : α →₀ β}
{h₁ h₂ : α → β → γ} :
@[simp]
theorem
finsupp.sum_neg
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
[add_comm_group γ]
{f : α →₀ β}
{h : α → β → γ} :
@[simp]
theorem
finsupp.sum_sub
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
[add_comm_group γ]
{f : α →₀ β}
{h₁ h₂ : α → β → γ} :
@[simp]
theorem
finsupp.sum_single
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid β]
(f : α →₀ β) :
f.sum finsupp.single = f
theorem
finsupp.sum_add_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
[add_comm_monoid γ]
{f g : α →₀ β}
{h : α → β → γ}
(h_zero : ∀ (a : α), h a 0 = 0)
(h_add : ∀ (a : α) (b₁ b₂ : β), h a (b₁ + b₂) = h a b₁ + h a b₂) :
theorem
finsupp.prod_add_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
[comm_monoid γ]
{f g : α →₀ β}
{h : α → β → γ}
(h_zero : ∀ (a : α), h a 0 = 1)
(h_add : ∀ (a : α) (b₁ b₂ : β), h a (b₁ + b₂) = (h a b₁) * h a b₂) :
theorem
finsupp.sum_sub_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_group β]
[add_comm_group γ]
{f g : α →₀ β}
{h : α → β → γ}
(h_sub : ∀ (a : α) (b₁ b₂ : β), h a (b₁ - b₂) = h a b₁ - h a b₂) :
theorem
finsupp.prod_finset_sum_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Type u_5}
[add_comm_monoid β]
[comm_monoid γ]
{s : finset ι}
{g : ι → α →₀ β}
{h : α → β → γ}
(h_zero : ∀ (a : α), h a 0 = 1)
(h_add : ∀ (a : α) (b₁ b₂ : β), h a (b₁ + b₂) = (h a b₁) * h a b₂) :
theorem
finsupp.sum_finset_sum_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Type u_5}
[add_comm_monoid β]
[add_comm_monoid γ]
{s : finset ι}
{g : ι → α →₀ β}
{h : α → β → γ}
(h_zero : ∀ (a : α), h a 0 = 0)
(h_add : ∀ (a : α) (b₁ b₂ : β), h a (b₁ + b₂) = h a b₁ + h a b₂) :
theorem
finsupp.sum_sum_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{α₁ : Type u_6}
{β₁ : Type u_8}
[add_comm_monoid β₁]
[add_comm_monoid β]
[add_comm_monoid γ]
{f : α₁ →₀ β₁}
{g : α₁ → β₁ → α →₀ β}
{h : α → β → γ}
(h_zero : ∀ (a : α), h a 0 = 0)
(h_add : ∀ (a : α) (b₁ b₂ : β), h a (b₁ + b₂) = h a b₁ + h a b₂) :
theorem
finsupp.prod_sum_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{α₁ : Type u_6}
{β₁ : Type u_8}
[add_comm_monoid β₁]
[add_comm_monoid β]
[comm_monoid γ]
{f : α₁ →₀ β₁}
{g : α₁ → β₁ → α →₀ β}
{h : α → β → γ}
(h_zero : ∀ (a : α), h a 0 = 1)
(h_add : ∀ (a : α) (b₁ b₂ : β), h a (b₁ + b₂) = (h a b₁) * h a b₂) :
theorem
finsupp.multiset_sum_sum_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
[add_comm_monoid γ]
(f : multiset (α →₀ β))
(h : α → β → γ)
(h₀ : ∀ (a : α), h a 0 = 0)
(h₁ : ∀ (a : α) (b₁ b₂ : β), h a (b₁ + b₂) = h a b₁ + h a b₂) :
theorem
finsupp.multiset_map_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[has_zero β]
{f : α →₀ β}
{m : γ → δ}
{h : α → β → multiset γ} :
multiset.map m (f.sum h) = f.sum (λ (a : α) (b : β), multiset.map m (h a b))
def
finsupp.map_range.add_monoid_hom
{α : Type u_1}
{β₁ : Type u_8}
{β₂ : Type u_9}
[add_comm_monoid β₁]
[add_comm_monoid β₂]
(f : β₁ →+ β₂) :
Composition with a fixed additive homomorphism is itself an additive homomorphism on functions.
Equations
- finsupp.map_range.add_monoid_hom f = {to_fun := finsupp.map_range ⇑f _, map_zero' := _, map_add' := _}
theorem
finsupp.map_range_multiset_sum
{α : Type u_1}
{β₁ : Type u_8}
{β₂ : Type u_9}
[add_comm_monoid β₁]
[add_comm_monoid β₂]
(f : β₁ →+ β₂)
(m : multiset (α →₀ β₁)) :
finsupp.map_range ⇑f _ m.sum = (multiset.map (λ (x : α →₀ β₁), finsupp.map_range ⇑f _ x) m).sum
theorem
finsupp.map_range_finset_sum
{α : Type u_1}
{β₁ : Type u_8}
{β₂ : Type u_9}
[add_comm_monoid β₁]
[add_comm_monoid β₂]
(f : β₁ →+ β₂)
{ι : Type u_2}
(s : finset ι)
(g : ι → α →₀ β₁) :
finsupp.map_range ⇑f _ (∑ (x : ι) in s, g x) = ∑ (x : ι) in s, finsupp.map_range ⇑f _ (g x)
Declarations about map_domain
def
finsupp.map_domain
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[add_comm_monoid β]
(f : α₁ → α₂)
(v : α₁ →₀ β) :
α₂ →₀ β
Given f : α₁ → α₂ and v : α₁ →₀ β, map_domain f v : α₂ →₀ β
is the finitely supported function whose value at a : α₂ is the sum
of v x over all x such that f x = a.
Equations
- finsupp.map_domain f v = v.sum (λ (a : α₁), finsupp.single (f a))
theorem
finsupp.map_domain_apply
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[add_comm_monoid β]
{f : α₁ → α₂}
(hf : function.injective f)
(x : α₁ →₀ β)
(a : α₁) :
⇑(finsupp.map_domain f x) (f a) = ⇑x a
theorem
finsupp.map_domain_notin_range
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[add_comm_monoid β]
{f : α₁ → α₂}
(x : α₁ →₀ β)
(a : α₂)
(h : a ∉ set.range f) :
⇑(finsupp.map_domain f x) a = 0
theorem
finsupp.map_domain_id
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid β]
{v : α →₀ β} :
finsupp.map_domain id v = v
theorem
finsupp.map_domain_comp
{α : Type u_1}
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[add_comm_monoid β]
{v : α →₀ β}
{f : α → α₁}
{g : α₁ → α₂} :
finsupp.map_domain (g ∘ f) v = finsupp.map_domain g (finsupp.map_domain f v)
theorem
finsupp.map_domain_single
{α : Type u_1}
{β : Type u_2}
{α₁ : Type u_6}
[add_comm_monoid β]
{f : α → α₁}
{a : α}
{b : β} :
finsupp.map_domain f (finsupp.single a b) = finsupp.single (f a) b
@[simp]
theorem
finsupp.map_domain_zero
{α : Type u_1}
{β : Type u_2}
{α₂ : Type u_7}
[add_comm_monoid β]
{f : α → α₂} :
finsupp.map_domain f 0 = 0
theorem
finsupp.map_domain_congr
{α : Type u_1}
{β : Type u_2}
{α₂ : Type u_7}
[add_comm_monoid β]
{v : α →₀ β}
{f g : α → α₂}
(h : ∀ (x : α), x ∈ v.support → f x = g x) :
finsupp.map_domain f v = finsupp.map_domain g v
theorem
finsupp.map_domain_add
{α : Type u_1}
{β : Type u_2}
{α₂ : Type u_7}
[add_comm_monoid β]
{v₁ v₂ : α →₀ β}
{f : α → α₂} :
finsupp.map_domain f (v₁ + v₂) = finsupp.map_domain f v₁ + finsupp.map_domain f v₂
theorem
finsupp.map_domain_finset_sum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
{α₂ : Type u_7}
[add_comm_monoid β]
{f : α → α₂}
{s : finset ι}
{v : ι → α →₀ β} :
finsupp.map_domain f (∑ (i : ι) in s, v i) = ∑ (i : ι) in s, finsupp.map_domain f (v i)
theorem
finsupp.map_domain_sum
{α : Type u_1}
{β : Type u_2}
{α₂ : Type u_7}
{β₁ : Type u_8}
[add_comm_monoid β]
[has_zero β₁]
{f : α → α₂}
{s : α →₀ β₁}
{v : α → β₁ → α →₀ β} :
finsupp.map_domain f (s.sum v) = s.sum (λ (a : α) (b : β₁), finsupp.map_domain f (v a b))
theorem
finsupp.map_domain_support
{α : Type u_1}
{β : Type u_2}
{α₂ : Type u_7}
[add_comm_monoid β]
{f : α → α₂}
{s : α →₀ β} :
(finsupp.map_domain f s).support ⊆ finset.image f s.support
theorem
finsupp.sum_map_domain_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{α₂ : Type u_7}
[add_comm_monoid β]
[add_comm_monoid γ]
{f : α → α₂}
{s : α →₀ β}
{h : α₂ → β → γ}
(h_zero : ∀ (a : α₂), h a 0 = 0)
(h_add : ∀ (a : α₂) (b₁ b₂ : β), h a (b₁ + b₂) = h a b₁ + h a b₂) :
(finsupp.map_domain f s).sum h = s.sum (λ (a : α) (b : β), h (f a) b)
theorem
finsupp.prod_map_domain_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{α₂ : Type u_7}
[add_comm_monoid β]
[comm_monoid γ]
{f : α → α₂}
{s : α →₀ β}
{h : α₂ → β → γ}
(h_zero : ∀ (a : α₂), h a 0 = 1)
(h_add : ∀ (a : α₂) (b₁ b₂ : β), h a (b₁ + b₂) = (h a b₁) * h a b₂) :
(finsupp.map_domain f s).prod h = s.prod (λ (a : α) (b : β), h (f a) b)
theorem
finsupp.emb_domain_eq_map_domain
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[add_comm_monoid β]
(f : α₁ ↪ α₂)
(v : α₁ →₀ β) :
finsupp.emb_domain f v = finsupp.map_domain ⇑f v
theorem
finsupp.map_domain_injective
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[add_comm_monoid β]
{f : α₁ → α₂}
(hf : function.injective f) :
Declarations about comap_domain
def
finsupp.comap_domain
{α₁ : Type u_1}
{α₂ : Type u_2}
{γ : Type u_3}
[has_zero γ]
(f : α₁ → α₂)
(l : α₂ →₀ γ)
(hf : set.inj_on f (f ⁻¹' ↑(l.support))) :
α₁ →₀ γ
Given f : α₁ → α₂, l : α₂ →₀ γ and a proof hf that f is injective on
the preimage of l.support, comap_domain f l hf is the finitely supported function
from α₁ to γ given by composing l with f.
Equations
- finsupp.comap_domain f l hf = {support := l.support.preimage f hf, to_fun := λ (a : α₁), ⇑l (f a), mem_support_to_fun := _}
@[simp]
theorem
finsupp.comap_domain_apply
{α₁ : Type u_1}
{α₂ : Type u_2}
{γ : Type u_3}
[has_zero γ]
(f : α₁ → α₂)
(l : α₂ →₀ γ)
(hf : set.inj_on f (f ⁻¹' ↑(l.support)))
(a : α₁) :
⇑(finsupp.comap_domain f l hf) a = ⇑l (f a)
theorem
finsupp.sum_comap_domain
{α₁ : Type u_1}
{α₂ : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_zero β]
[add_comm_monoid γ]
(f : α₁ → α₂)
(l : α₂ →₀ β)
(g : α₂ → β → γ)
(hf : set.bij_on f (f ⁻¹' ↑(l.support)) ↑(l.support)) :
(finsupp.comap_domain f l _).sum (g ∘ f) = l.sum g
theorem
finsupp.eq_zero_of_comap_domain_eq_zero
{α₁ : Type u_1}
{α₂ : Type u_2}
{γ : Type u_3}
[add_comm_monoid γ]
(f : α₁ → α₂)
(l : α₂ →₀ γ)
(hf : set.bij_on f (f ⁻¹' ↑(l.support)) ↑(l.support))
(a : finsupp.comap_domain f l _ = 0) :
l = 0
theorem
finsupp.map_domain_comap_domain
{α₁ : Type u_1}
{α₂ : Type u_2}
{γ : Type u_3}
[add_comm_monoid γ]
(f : α₁ → α₂)
(l : α₂ →₀ γ)
(hf : function.injective f)
(hl : ↑(l.support) ⊆ set.range f) :
finsupp.map_domain f (finsupp.comap_domain f l _) = l
Declarations about filter
filter p f is the function which is f a if p a is true and 0 otherwise.
Equations
- finsupp.filter p f = finsupp.on_finset f.support (λ (a : α), ite (p a) (⇑f a) 0) _
@[simp]
theorem
finsupp.filter_apply_pos
{α : Type u_1}
{β : Type u_2}
[has_zero β]
(p : α → Prop)
(f : α →₀ β)
{a : α}
(h : p a) :
⇑(finsupp.filter p f) a = ⇑f a
@[simp]
theorem
finsupp.filter_apply_neg
{α : Type u_1}
{β : Type u_2}
[has_zero β]
(p : α → Prop)
(f : α →₀ β)
{a : α}
(h : ¬p a) :
⇑(finsupp.filter p f) a = 0
@[simp]
theorem
finsupp.support_filter
{α : Type u_1}
{β : Type u_2}
[has_zero β]
(p : α → Prop)
(f : α →₀ β) :
(finsupp.filter p f).support = finset.filter p f.support
theorem
finsupp.filter_zero
{α : Type u_1}
{β : Type u_2}
[has_zero β]
(p : α → Prop) :
finsupp.filter p 0 = 0
@[simp]
theorem
finsupp.filter_single_of_pos
{α : Type u_1}
{β : Type u_2}
[has_zero β]
(p : α → Prop)
{a : α}
{b : β}
(h : p a) :
finsupp.filter p (finsupp.single a b) = finsupp.single a b
@[simp]
theorem
finsupp.filter_single_of_neg
{α : Type u_1}
{β : Type u_2}
[has_zero β]
(p : α → Prop)
{a : α}
{b : β}
(h : ¬p a) :
finsupp.filter p (finsupp.single a b) = 0
theorem
finsupp.filter_pos_add_filter_neg
{α : Type u_1}
{β : Type u_2}
[add_monoid β]
(f : α →₀ β)
(p : α → Prop) :
finsupp.filter p f + finsupp.filter (λ (a : α), ¬p a) f = f
Declarations about frange
frange f is the image of f on the support of f.
Equations
- f.frange = finset.image ⇑f f.support
theorem
finsupp.frange_single
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{x : α}
{y : β} :
(finsupp.single x y).frange ⊆ {y}
Declarations about subtype_domain
subtype_domain p f is the restriction of the finitely supported function
f to the subtype p.
Equations
- finsupp.subtype_domain p f = {support := finset.subtype p f.support, to_fun := ⇑f ∘ subtype.val, mem_support_to_fun := _}
@[simp]
theorem
finsupp.support_subtype_domain
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
[has_zero β]
{f : α →₀ β} :
(finsupp.subtype_domain p f).support = finset.subtype p f.support
@[simp]
theorem
finsupp.subtype_domain_apply
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
[has_zero β]
{a : subtype p}
{v : α →₀ β} :
⇑(finsupp.subtype_domain p v) a = ⇑v a.val
@[simp]
theorem
finsupp.subtype_domain_zero
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
[has_zero β] :
finsupp.subtype_domain p 0 = 0
theorem
finsupp.sum_subtype_domain_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{p : α → Prop}
[has_zero β]
[add_comm_monoid γ]
{v : α →₀ β}
{h : α → β → γ}
(hp : ∀ (x : α), x ∈ v.support → p x) :
theorem
finsupp.prod_subtype_domain_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{p : α → Prop}
[has_zero β]
[comm_monoid γ]
{v : α →₀ β}
{h : α → β → γ}
(hp : ∀ (x : α), x ∈ v.support → p x) :
@[simp]
theorem
finsupp.subtype_domain_add
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
[add_monoid β]
{v v' : α →₀ β} :
finsupp.subtype_domain p (v + v') = finsupp.subtype_domain p v + finsupp.subtype_domain p v'
@[instance]
def
finsupp.subtype_domain.is_add_monoid_hom
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
[add_monoid β] :
@[simp]
theorem
finsupp.filter_add
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
[add_monoid β]
{v v' : α →₀ β} :
finsupp.filter p (v + v') = finsupp.filter p v + finsupp.filter p v'
@[instance]
theorem
finsupp.subtype_domain_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{p : α → Prop}
[add_comm_monoid β]
{s : finset γ}
{h : γ → α →₀ β} :
finsupp.subtype_domain p (∑ (c : γ) in s, h c) = ∑ (c : γ) in s, finsupp.subtype_domain p (h c)
theorem
finsupp.subtype_domain_finsupp_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[has_zero δ]
{p : α → Prop}
[add_comm_monoid β]
{s : γ →₀ δ}
{h : γ → δ → α →₀ β} :
finsupp.subtype_domain p (s.sum h) = s.sum (λ (c : γ) (d : δ), finsupp.subtype_domain p (h c d))
theorem
finsupp.filter_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{p : α → Prop}
[add_comm_monoid β]
(s : finset γ)
(f : γ → α →₀ β) :
finsupp.filter p (∑ (a : γ) in s, f a) = ∑ (a : γ) in s, finsupp.filter p (f a)
@[simp]
theorem
finsupp.subtype_domain_neg
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
[add_group β]
{v : α →₀ β} :
finsupp.subtype_domain p (-v) = -finsupp.subtype_domain p v
@[simp]
theorem
finsupp.subtype_domain_sub
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
[add_group β]
{v v' : α →₀ β} :
finsupp.subtype_domain p (v - v') = finsupp.subtype_domain p v - finsupp.subtype_domain p v'
Given f : α →₀ ℕ, f.to_multiset is the multiset with multiplicities given by the values of
f on the elements of α.
Equations
- f.to_multiset = f.sum (λ (a : α) (n : ℕ), n •ℕ {a})
@[simp]
theorem
finsupp.to_multiset_add
{α : Type u_1}
(m n : α →₀ ℕ) :
(m + n).to_multiset = m.to_multiset + n.to_multiset
theorem
finsupp.to_multiset_single
{α : Type u_1}
(a : α)
(n : ℕ) :
(finsupp.single a n).to_multiset = n •ℕ {a}
@[instance]
theorem
finsupp.card_to_multiset
{α : Type u_1}
(f : α →₀ ℕ) :
f.to_multiset.card = f.sum (λ (a : α), id)
theorem
finsupp.to_multiset_map
{α : Type u_1}
{β : Type u_2}
(f : α →₀ ℕ)
(g : α → β) :
multiset.map g f.to_multiset = (finsupp.map_domain g f).to_multiset
theorem
finsupp.to_finset_to_multiset
{α : Type u_1}
(f : α →₀ ℕ) :
f.to_multiset.to_finset = f.support
@[simp]
theorem
finsupp.count_to_multiset
{α : Type u_1}
(f : α →₀ ℕ)
(a : α) :
multiset.count a f.to_multiset = ⇑f a
Given m : multiset α, of_multiset m is the finitely supported function from α to ℕ
given by the multiplicities of the elements of α in m.
Equations
- finsupp.of_multiset m = finsupp.on_finset m.to_finset (λ (a : α), multiset.count a m) _
@[simp]
theorem
finsupp.of_multiset_apply
{α : Type u_1}
(m : multiset α)
(a : α) :
⇑(finsupp.of_multiset m) a = multiset.count a m
equiv_multiset defines an equiv between finitely supported functions
from α to ℕ and multisets on α.
Equations
- finsupp.equiv_multiset = {to_fun := finsupp.to_multiset α, inv_fun := finsupp.of_multiset α, left_inv := _, right_inv := _}
theorem
finsupp.mem_support_finset_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
{s : finset γ}
{h : γ → α →₀ β}
(a : α)
(ha : a ∈ (∑ (c : γ) in s, h c).support) :
@[simp]
theorem
finsupp.mem_to_multiset
{α : Type u_1}
(f : α →₀ ℕ)
(i : α) :
i ∈ f.to_multiset ↔ i ∈ f.support
Declarations about curry and uncurry
def
finsupp.curry
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid γ]
(f : α × β →₀ γ) :
Given a finitely supported function f from a product type α × β to γ,
curry f is the "curried" finitely supported function from α to the type of
finitely supported functions from β to γ.
Equations
- f.curry = f.sum (λ (p : α × β) (c : γ), finsupp.single p.fst (finsupp.single p.snd c))
theorem
finsupp.sum_curry_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[add_comm_monoid γ]
[add_comm_monoid δ]
(f : α × β →₀ γ)
(g : α → β → γ → δ)
(hg₀ : ∀ (a : α) (b : β), g a b 0 = 0)
(hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : γ), g a b (c₀ + c₁) = g a b c₀ + g a b c₁) :
def
finsupp.uncurry
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid γ]
(f : α →₀ β →₀ γ) :
Given a finitely supported function f from α to the type of
finitely supported functions from β to γ,
uncurry f is the "uncurried" finitely supported function from α × β to γ.
finsupp_prod_equiv defines the equiv between ((α × β) →₀ γ) and (α →₀ (β →₀ γ)) given by
currying and uncurrying.
Equations
- finsupp.finsupp_prod_equiv = {to_fun := finsupp.curry _inst_1, inv_fun := finsupp.uncurry _inst_1, left_inv := _, right_inv := _}
theorem
finsupp.filter_curry
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[add_comm_monoid β]
(f : α₁ × α₂ →₀ β)
(p : α₁ → Prop) :
(finsupp.filter (λ (a : α₁ × α₂), p a.fst) f).curry = finsupp.filter p f.curry
theorem
finsupp.support_curry
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[add_comm_monoid β]
(f : α₁ × α₂ →₀ β) :
def
finsupp.comap_has_scalar
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[group γ]
[mul_action γ α]
[add_comm_monoid β] :
has_scalar γ (α →₀ β)
Scalar multiplication by a group element g, given by precomposition with the action of g⁻¹ on the domain.
Equations
- finsupp.comap_has_scalar = {smul := λ (g : γ) (f : α →₀ β), finsupp.comap_domain (λ (a : α), g⁻¹ • a) f _}
def
finsupp.comap_mul_action
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[group γ]
[mul_action γ α]
[add_comm_monoid β] :
mul_action γ (α →₀ β)
Scalar multiplication by a group element, given by precomposition with the action of g⁻¹ on the domain, is multiplicative in g.
Equations
- finsupp.comap_mul_action = {to_has_scalar := finsupp.comap_has_scalar _inst_3, one_smul := _, mul_smul := _}
def
finsupp.comap_distrib_mul_action
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[group γ]
[mul_action γ α]
[add_comm_monoid β] :
distrib_mul_action γ (α →₀ β)
Scalar multiplication by a group element, given by precomposition with the action of g⁻¹ on the domain, is additive in the second argument.
Equations
- finsupp.comap_distrib_mul_action = {to_mul_action := finsupp.comap_mul_action _inst_3, smul_add := _, smul_zero := _}
def
finsupp.comap_distrib_mul_action_self
{β : Type u_2}
{γ : Type u_3}
[group γ]
[add_comm_monoid β] :
distrib_mul_action γ (γ →₀ β)
Scalar multiplication by a group element on finitely supported functions on a group, given by precomposition with the action of g⁻¹.
@[simp]
theorem
finsupp.comap_smul_single
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[group γ]
[mul_action γ α]
[add_comm_monoid β]
(g : γ)
(a : α)
(b : β) :
g • finsupp.single a b = finsupp.single (g • a) b
@[simp]
theorem
finsupp.comap_smul_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[group γ]
[mul_action γ α]
[add_comm_monoid β]
(g : γ)
(f : α →₀ β)
(a : α) :
@[instance]
def
finsupp.has_scalar
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semiring γ]
[add_comm_monoid β]
[semimodule γ β] :
has_scalar γ (α →₀ β)
Equations
- finsupp.has_scalar = {smul := λ (a : γ) (v : α →₀ β), finsupp.map_range (has_scalar.smul a) _ v}
@[simp]
theorem
finsupp.smul_apply'
(α : Type u_1)
(β : Type u_2)
{γ : Type u_3}
{R : semiring γ}
[add_comm_monoid β]
[semimodule γ β]
{a : α}
{b : γ}
{v : α →₀ β} :
@[instance]
def
finsupp.semimodule
(α : Type u_1)
(β : Type u_2)
{γ : Type u_3}
[semiring γ]
[add_comm_monoid β]
[semimodule γ β] :
semimodule γ (α →₀ β)
Equations
- finsupp.semimodule α β = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul finsupp.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
def
finsupp.leval'
{α : Type u_1}
{β : Type u_2}
(γ : Type u_3)
[semiring γ]
[add_comm_monoid β]
[semimodule γ β]
(a : α) :
Evaluation at point as a linear map. This version assumes that the codomain is a semimodule
over some semiring. See also leval.
@[simp]
theorem
finsupp.coe_leval'
{α : Type u_1}
{β : Type u_2}
(γ : Type u_3)
[semiring γ]
[add_comm_monoid β]
[semimodule γ β]
(a : α)
(g : α →₀ β) :
⇑(finsupp.leval' γ a) g = ⇑g a
Evaluation at point as a linear map. This version assumes that the codomain is a semiring.
Equations
- finsupp.leval a = finsupp.leval' β a
@[simp]
theorem
finsupp.coe_leval
{α : Type u_1}
{β : Type u_2}
[semiring β]
(a : α)
(g : α →₀ β) :
⇑(finsupp.leval a) g = ⇑g a
theorem
finsupp.support_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{R : semiring γ}
[add_comm_monoid β]
[semimodule γ β]
{b : γ}
{g : α →₀ β} :
@[simp]
theorem
finsupp.filter_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{p : α → Prop}
{R : semiring γ}
[add_comm_monoid β]
[semimodule γ β]
{b : γ}
{v : α →₀ β} :
finsupp.filter p (b • v) = b • finsupp.filter p v
theorem
finsupp.map_domain_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{α' : Type u_4}
{R : semiring γ}
[add_comm_monoid β]
[semimodule γ β]
{f : α → α'}
(b : γ)
(v : α →₀ β) :
finsupp.map_domain f (b • v) = b • finsupp.map_domain f v
@[simp]
theorem
finsupp.smul_single
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{R : semiring γ}
[add_comm_monoid β]
[semimodule γ β]
(c : γ)
(a : α)
(b : β) :
c • finsupp.single a b = finsupp.single a (c • b)
@[simp]
theorem
finsupp.smul_single'
{α : Type u_1}
{γ : Type u_3}
{R : semiring γ}
(c : γ)
(a : α)
(b : γ) :
c • finsupp.single a b = finsupp.single a (c * b)
theorem
finsupp.smul_single_one
{α : Type u_1}
{β : Type u_2}
[semiring β]
(a : α)
(b : β) :
b • finsupp.single a 1 = finsupp.single a b
theorem
finsupp.hom_ext
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semiring β]
[add_comm_monoid γ]
[semimodule β γ]
(φ ψ : (α →₀ β) →ₗ[β] γ)
(h : ∀ (a : α), ⇑φ (finsupp.single a 1) = ⇑ψ (finsupp.single a 1)) :
φ = ψ
Two R-linear maps from finsupp X R which agree on single x 1 agree everywhere.
theorem
finsupp.sum_smul_index'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[semiring β]
[add_comm_monoid γ]
[semimodule β γ]
[add_comm_monoid δ]
{g : α →₀ γ}
{b : β}
{h : α → γ → δ}
(h0 : ∀ (i : α), h i 0 = 0) :
Given an add_comm_monoid β and s : set α, restrict_support_equiv s β is the equiv
between the subtype of finitely supported functions with support contained in s and
the type of finitely supported functions from s.
Equations
- finsupp.restrict_support_equiv s β = {to_fun := λ (f : {f // ↑(f.support) ⊆ s}), finsupp.subtype_domain (λ (x : α), x ∈ s) f.val, inv_fun := λ (f : ↥s →₀ β), ⟨finsupp.map_domain subtype.val f, _⟩, left_inv := _, right_inv := _}
def
finsupp.dom_congr
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
[add_comm_monoid β]
(e : α₁ ≃ α₂) :
Given add_comm_monoid β and e : α₁ ≃ α₂, dom_congr e is the corresponding equiv between
α₁ →₀ β and α₂ →₀ β.
Equations
- finsupp.dom_congr e = {to_fun := finsupp.map_domain ⇑e, inv_fun := finsupp.map_domain ⇑(e.symm), left_inv := _, right_inv := _}
Declarations about sigma types
def
finsupp.split
{β : Type u_2}
{ι : Type u_5}
{αs : ι → Type u_10}
[has_zero β]
(l : (Σ (i : ι), αs i) →₀ β)
(i : ι) :
αs i →₀ β
Given l, a finitely supported function from the sigma type Σ (i : ι), αs i to β and
an index element i : ι, split l i is the ith component of l,
a finitely supported function from as i to β.
Equations
- l.split i = finsupp.comap_domain (sigma.mk i) l _
def
finsupp.split_support
{β : Type u_2}
{ι : Type u_5}
{αs : ι → Type u_10}
[has_zero β]
(l : (Σ (i : ι), αs i) →₀ β) :
finset ι
Given l, a finitely supported function from the sigma type Σ (i : ι), αs i to β,
split_support l is the finset of indices in ι that appear in the support of l.
Equations
theorem
finsupp.mem_split_support_iff_nonzero
{β : Type u_2}
{ι : Type u_5}
{αs : ι → Type u_10}
[has_zero β]
(l : (Σ (i : ι), αs i) →₀ β)
(i : ι) :
i ∈ l.split_support ↔ l.split i ≠ 0
def
finsupp.split_comp
{β : Type u_2}
{γ : Type u_3}
{ι : Type u_5}
{αs : ι → Type u_10}
[has_zero β]
(l : (Σ (i : ι), αs i) →₀ β)
[has_zero γ]
(g : Π (i : ι), (αs i →₀ β) → γ)
(hg : ∀ (i : ι) (x : αs i →₀ β), x = 0 ↔ g i x = 0) :
ι →₀ γ
Given l, a finitely supported function from the sigma type Σ i, αs i to β and
an ι-indexed family g of functions from (αs i →₀ β) to γ, split_comp defines a
finitely supported function from the index type ι to γ given by composing g i with
split l i.
Equations
- l.split_comp g hg = {support := l.split_support, to_fun := λ (i : ι), g i (l.split i), mem_support_to_fun := _}
theorem
finsupp.sigma_support
{β : Type u_2}
{ι : Type u_5}
{αs : ι → Type u_10}
[has_zero β]
(l : (Σ (i : ι), αs i) →₀ β) :
theorem
finsupp.sigma_sum
{β : Type u_2}
{γ : Type u_3}
{ι : Type u_5}
{αs : ι → Type u_10}
[has_zero β]
(l : (Σ (i : ι), αs i) →₀ β)
[add_comm_monoid γ]
(f : (Σ (i : ι), αs i) → β → γ) :
Given a multiset s, s.to_finsupp returns the finitely supported function on ℕ given by
the multiplicities of the elements of s.
Equations
- s.to_finsupp = {support := s.to_finset, to_fun := λ (a : α), multiset.count a s, mem_support_to_fun := _}
@[simp]
theorem
multiset.to_finsupp_support
{α : Type u_1}
(s : multiset α) :
s.to_finsupp.support = s.to_finset
@[simp]
theorem
multiset.to_finsupp_apply
{α : Type u_1}
(s : multiset α)
(a : α) :
⇑(s.to_finsupp) a = multiset.count a s
@[simp]
theorem
multiset.to_finsupp_add
{α : Type u_1}
(s t : multiset α) :
(s + t).to_finsupp = s.to_finsupp + t.to_finsupp
@[instance]
@[simp]
theorem
multiset.to_finsupp_to_multiset
{α : Type u_1}
(s : multiset α) :
s.to_finsupp.to_multiset = s
Declarations about order(ed) instances on finsupp
@[instance]
@[instance]
def
finsupp.partial_order
{α : Type u_1}
{σ : Type u_10}
[partial_order α]
[has_zero α] :
partial_order (σ →₀ α)
Equations
- finsupp.partial_order = {le := preorder.le finsupp.preorder, lt := preorder.lt finsupp.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[instance]
def
finsupp.add_left_cancel_semigroup
{α : Type u_1}
{σ : Type u_10}
[ordered_cancel_add_comm_monoid α] :
add_left_cancel_semigroup (σ →₀ α)
Equations
@[instance]
def
finsupp.add_right_cancel_semigroup
{α : Type u_1}
{σ : Type u_10}
[ordered_cancel_add_comm_monoid α] :
add_right_cancel_semigroup (σ →₀ α)
Equations
@[instance]
def
finsupp.ordered_cancel_add_comm_monoid
{α : Type u_1}
{σ : Type u_10}
[ordered_cancel_add_comm_monoid α] :
Equations
- finsupp.ordered_cancel_add_comm_monoid = {add := add_comm_monoid.add finsupp.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero finsupp.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, add_left_cancel := _, add_right_cancel := _, le := partial_order.le finsupp.partial_order, lt := partial_order.lt finsupp.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}
@[simp]
theorem
finsupp.add_eq_zero_iff
{α : Type u_1}
{σ : Type u_10}
[canonically_ordered_add_monoid α]
(f g : σ →₀ α) :
@[simp]
The order on σ →₀ ℕ is well-founded.
@[instance]
Equations
- finsupp.decidable_le σ = λ (m n : σ →₀ ℕ), _.mpr finset.decidable_dforall_finset
The finsupp counterpart of multiset.antidiagonal: the antidiagonal of
s : σ →₀ ℕ consists of all pairs (t₁, t₂) : (σ →₀ ℕ) × (σ →₀ ℕ) such that t₁ + t₂ = s.
The finitely supported function antidiagonal s is equal to the multiplicities of these pairs.
Equations
@[simp]