no goals
α : Type u
R : Type v
inst✝ : CommRing R
f✝ : α → R
f : FreeCommRing α →+* R
x : FreeCommRing α
⊢ ↑(↑lift (↑f ∘ of)) (-1) = ↑f (-1)
rw [RingHom.map_neg, RingHom.map_one, f.map_neg, f.map_one]
no goals
α : Type u
R : Type v
inst✝ : CommRing R
f✝ : α → R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : ↑(↑lift (↑f ∘ of)) x = ↑f x
ihy : ↑(↑lift (↑f ∘ of)) y = ↑f y
⊢ ↑(↑lift (↑f ∘ of)) (x + y) = ↑f (x + y)
rw [RingHom.map_add, f.map_add, ihx, ihy]
no goals
α : Type u
R : Type v
inst✝ : CommRing R
f✝ : α → R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : ↑(↑lift (↑f ∘ of)) x = ↑f x
ihy : ↑(↑lift (↑f ∘ of)) y = ↑f y
⊢ ↑(↑lift (↑f ∘ of)) (x * y) = ↑f (x * y)
rw [RingHom.map_mul, f.map_mul, ihx, ihy]