no goals
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_1
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)
rw [abv.map_units_int_smul, abv.map_prod]
no goals
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_1
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
rw [prod_const, Finset.card_univ]
no goals
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_1
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
rw [sum_const, Finset.card_univ, Fintype.card_perm]