no goals
R✝ : Type u
inst✝³ : CommMonoid R✝
R' : Type v
inst✝² : CommMonoidWithZero R'
R : Type u
inst✝¹ : CommMonoidWithZero R
inst✝ : Nontrivial R
χ : MulChar R R'
⊢ ↑χ 0 = 0
rw [map_nonunit χ not_isUnit_zero]