[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), ↑abv (A i j) ≤ x
σ : Perm n
x✝ : σ ∈ univ
⊢ ↑abv (↑Perm.sign σ • ∏ i : n, A (↑σ i) i) = ∏ i : n, ↑abv (A (↑σ i) i)
[PROOFSTEP]
rw [abv.map_units_int_smul, abv.map_prod]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), ↑abv (A i j) ≤ x
x✝¹ : Perm n
x✝ : x✝¹ ∈ univ
⊢ ∏ _i : n, x = x ^ Fintype.card n
[PROOFSTEP]
rw [prod_const, Finset.card_univ]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), ↑abv (A i j) ≤ x
⊢ ∑ _σ : Perm n, x ^ Fintype.card n = Nat.factorial (Fintype.card n) • x ^ Fintype.card n
[PROOFSTEP]
rw [sum_const, Finset.card_univ, Fintype.card_perm]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
ι : Type u_4
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)
[PROOFSTEP]
simp only [sum_apply]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
ι : Type u_4
s : Finset ι
c : ι → R
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), ↑abv (A k i j) ≤ x
y : S
hy : ∀ (k : ι), ↑abv (c k) ≤ y
⊢ ↑abv (det (∑ k in s, c k • A k)) ≤ Nat.factorial (Fintype.card n) • (card s • y * x) ^ Fintype.card n
[PROOFSTEP]
simpa only [smul_mul_assoc] using
  det_sum_le s fun k i j =>
    calc
      abv (c k * A k i j) = abv (c k) * abv (A k i j) := abv.map_mul _ _
      _ ≤ y * x := mul_le_mul (hy k) (hx k i j) (abv.nonneg _) ((abv.nonneg _).trans (hy k))
