∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [Nontrivial R] [inst_2 : CommRing S]
  [inst_3 : LinearOrder S] [IsStrictOrderedRing S] (abv : R → S) [IsAbsoluteValue abv] (f : ι → R) (s : Finset ι),
  abv (∏ i ∈ s, f i) = ∏ i ∈ s, abv (f i)