case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ support (↑(opRingEquiv R) (op p)) = support (unop (op p))
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ support (↑(opRingEquiv R) p) = support (unop p)
induction' p using MulOpposite.rec' with p
case h.ofFinsupp
R : Type u_1
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (↑(opRingEquiv R) (op { toFinsupp := toFinsupp✝ })) = support (unop (op { toFinsupp := toFinsupp✝ }))
case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ support (↑(opRingEquiv R) (op p)) = support (unop (op p))
cases p
no goals
case h.ofFinsupp
R : Type u_1
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (↑(opRingEquiv R) (op { toFinsupp := toFinsupp✝ })) = support (unop (op { toFinsupp := toFinsupp✝ }))
exact Finsupp.support_mapRange_of_injective (map_zero _) _ op_injective