Theorem: to_MvPolynomial_Option_C (FormalSnarksProject/ToMathlib/OptionEquivRight.lean)

State before:
F V : Type
inst✝ : Field F
r : F
⊢ (to_MvPolynomial_Option V) (Polynomial.C r) = C r
Tactic:
simp [to_MvPolynomial_Option]
State after:
no goals