case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x✝ : Γ'
⊢ coeff (embDomain f 0) x✝ = coeff 0 x✝
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
⊢ embDomain f 0 = 0
ext
no goals
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x✝ : Γ'
⊢ coeff (embDomain f 0) x✝ = coeff 0 x✝
simp [embDomain_notin_image_support]