Lifts a Finsupp from an underlying type to a Finsupp on a quotient

noncomputable def Quot.liftFinsupp {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [Zero β] (f : α →₀ β) (h : ∀ (a b : α), r a b → f a = f b) : Quot r →₀ β

Lift a function α →₀ β to Quot r →₀ β.

Equations

• Quot.liftFinsupp f h = { support := Finset.image (Quot.mk r) f.support, toFun := Quot.lift (⇑f) h, mem_support_toFun := ⋯ }

@[simp]

theorem Quot.liftFinsupp_mk {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [Zero β] (f : α →₀ β) (h : ∀ (a b : α), r a b → f a = f b) (a : α) : (Quot.liftFinsupp f h) (mk r a) = f a

noncomputable def Quotient.liftFinsupp {α : Type u_1} {β : Type u_2} {s : Setoid α} [Zero β] (f : α →₀ β) (h : ∀ (a b : α), s a b → f a = f b) : Quotient s →₀ β

Lift a function α →₀ β to Quot r →₀ β.

Equations

• Quotient.liftFinsupp f h = Quot.liftFinsupp f h

@[simp]

theorem Quotient.liftFinsupp_mk {α : Type u_1} {β : Type u_2} {s : Setoid α} [Zero β] (f : α →₀ β) (h : ∀ (a b : α), s a b → f a = f b) (a : α) : (Quotient.liftFinsupp f h) ⟦a⟧ = f a