# mathlib3documentation

linear_algebra.matrix.absolute_value

# Absolute values and matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves some bounds on matrices involving absolute values.

## Main results #

• matrix.det_le: if the entries of an n × n matrix are bounded by x, then the determinant is bounded by n! x^n
• matrix.det_sum_le: if we have s n × n matrices and the entries of each matrix are bounded by x, then the determinant of their sum is bounded by n! (s * x)^n
• matrix.det_sum_smul_le: if we have s n × n matrices each multiplied by a constant bounded by y, and the entries of each matrix are bounded by x, then the determinant of the linear combination is bounded by n! (s * y * x)^n
theorem matrix.det_le {R : Type u_1} {S : Type u_2} [comm_ring R] [nontrivial R] {n : Type u_3} [fintype n] [decidable_eq n] {A : n R} {abv : S} {x : S} (hx : (i j : n), abv (A i j) x) :
abv A.det
theorem matrix.det_sum_le {R : Type u_1} {S : Type u_2} [comm_ring R] [nontrivial R] {n : Type u_3} [fintype n] [decidable_eq n] {ι : Type u_4} (s : finset ι) {A : ι n R} {abv : S} {x : S} (hx : (k : ι) (i j : n), abv (A k i j) x) :
abv (s.sum (λ (k : ι), A k)).det (s.card x) ^
theorem matrix.det_sum_smul_le {R : Type u_1} {S : Type u_2} [comm_ring R] [nontrivial R] {n : Type u_3} [fintype n] [decidable_eq n] {ι : Type u_4} (s : finset ι) {c : ι R} {A : ι n R} {abv : S} {x : S} (hx : (k : ι) (i j : n), abv (A k i j) x) {y : S} (hy : (k : ι), abv (c k) y) :
abv (s.sum (λ (k : ι), c k A k)).det (s.card y * x) ^