Pi-types of star-ordered rings

instance Pi.instStarOrderedRing {ι : Type u_1} [Finite ι] {A : ι → Type u_2} [(i : ι) → PartialOrder (A i)] [(i : ι) → NonUnitalSemiring (A i)] [(i : ι) → StarRing (A i)] [∀ (i : ι), StarOrderedRing (A i)] : StarOrderedRing ((i : ι) → A i)