no goals
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
ι : Type u_1
s : Finset ι
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), ↑abv (A k i j) ≤ x
i j : n
⊢ ↑abv (Finset.sum s (fun k => A k) i j) = ↑abv (∑ k in s, A k i j)
simp only [sum_apply]