Finiteness of the multiplicative opposite

MulOpposite α carries no multiplication of its own here: it is finite exactly when α is.

instance MulOpposite.instFinite {α : Type u_1} [Finite α] : Finite αᵐᵒᵖ