linear_algebra.determinant

source

noncomputable def equiv_of_pi_lequiv_pi {m : Type u_6} {n : Type u_7} [fintype m] [fintype n] {R : Type u_1} [comm_ring R] [nontrivial R] (e : (m → R) ≃ₗ[R] n → R) :

m ≃ n

If R^m and R^n are linearly equivalent, then m and n are also equivalent.

Equations

equiv_of_pi_lequiv_pi e = (basis.of_equiv_fun e.symm).index_equiv (pi.basis_fun R n)

source

noncomputable def matrix.index_equiv_of_inv {A : Type u_5} [comm_ring A] {m : Type u_6} {n : Type u_7} [fintype m] [fintype n] [nontrivial A] [decidable_eq m] [decidable_eq n] {M : matrix m n A} {M' : matrix n m A} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) :

m ≃ n

If M and M' are each other's inverse matrices, they are square matrices up to equivalence of types.

Equations

matrix.index_equiv_of_inv hMM' hM'M = equiv_of_pi_lequiv_pi (matrix.to_lin'_of_inv hMM' hM'M)

source

theorem matrix.det_comm {A : Type u_5} [comm_ring A] {n : Type u_7} [fintype n] [decidable_eq n] (M N : matrix n n A) :

(M.mul N).det = (N.mul M).det

source

theorem matrix.det_comm' {A : Type u_5} [comm_ring A] {m : Type u_6} {n : Type u_7} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] {M : matrix n m A} {N M' : matrix m n A} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) :

(M.mul N).det = (N.mul M).det

If there exists a two-sided inverse M' for M (indexed differently), then det (N ⬝ M) = det (M ⬝ N).

source

theorem matrix.det_conj_of_mul_eq_one {A : Type u_5} [comm_ring A] {m : Type u_6} {n : Type u_7} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] {M : matrix m n A} {M' : matrix n m A} {N : matrix n n A} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) :

((M.mul N).mul M').det = N.det

If M' is a two-sided inverse for M (indexed differently), det (M ⬝ N ⬝ M') = det N.

See matrix.det_conj and matrix.det_conj' for the case when M' = M⁻¹ or vice versa.

source

theorem linear_map.det_to_matrix_eq_det_to_matrix {M : Type u_2} [add_comm_group M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [comm_ring A] [module A M] {κ : Type u_6} [fintype κ] [decidable_eq κ] (b : basis ι A M) (c : basis κ A M) (f : M →ₗ[A] M) :

(⇑(linear_map.to_matrix b b) f).det = (⇑(linear_map.to_matrix c c) f).det

The determinant of linear_map.to_matrix does not depend on the choice of basis.

source

@[irreducible]

noncomputable def linear_map.det_aux {M : Type u_2} [add_comm_group M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [comm_ring A] [module A M] :

trunc (basis ι A M) → (M →ₗ[A] M) →* A

The determinant of an endomorphism given a basis.

See linear_map.det for a version that populates the basis non-computably.

Although the trunc (basis ι A M) parameter makes it slightly more convenient to switch bases, there is no good way to generalize over universe parameters, so we can't fully state in det_aux's type that it does not depend on the choice of basis. Instead you can use the det_aux_def' lemma, or avoid mentioning a basis at all using linear_map.det.

Equations

linear_map.det_aux = trunc.lift (λ (b : basis ι A M), matrix.det_monoid_hom.comp ↑(linear_map.to_matrix_alg_equiv b)) linear_map.det_aux._proof_1

source

theorem linear_map.det_aux_def {M : Type u_2} [add_comm_group M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [comm_ring A] [module A M] (b : basis ι A M) (f : M →ₗ[A] M) :

⇑(linear_map.det_aux (trunc.mk b)) f = (⇑(linear_map.to_matrix b b) f).det

Unfold lemma for det_aux.

See also det_aux_def' which allows you to vary the basis.

source

theorem linear_map.det_aux_def' {M : Type u_2} [add_comm_group M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [comm_ring A] [module A M] {ι' : Type u_1} [fintype ι'] [decidable_eq ι'] (tb : trunc (basis ι A M)) (b' : basis ι' A M) (f : M →ₗ[A] M) :

⇑(linear_map.det_aux tb) f = (⇑(linear_map.to_matrix b' b') f).det

source

@[simp]

theorem linear_map.det_aux_id {M : Type u_2} [add_comm_group M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [comm_ring A] [module A M] (b : trunc (basis ι A M)) :

⇑(linear_map.det_aux b) linear_map.id = 1

source

@[simp]

theorem linear_map.det_aux_comp {M : Type u_2} [add_comm_group M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [comm_ring A] [module A M] (b : trunc (basis ι A M)) (f g : M →ₗ[A] M) :

⇑(linear_map.det_aux b) (f.comp g) = ⇑(linear_map.det_aux b) f * ⇑(linear_map.det_aux b) g

source

@[protected, irreducible]

noncomputable def linear_map.det {M : Type u_2} [add_comm_group M] {A : Type u_5} [comm_ring A] [module A M] :

(M →ₗ[A] M) →* A

The determinant of an endomorphism independent of basis.

If there is no finite basis on M, the result is 1 instead.

Equations

linear_map.det = dite (∃ (s : finset M), nonempty (basis ↥s A M)) (λ (H : ∃ (s : finset M), nonempty (basis ↥s A M)), linear_map.det_aux (trunc.mk (nonempty.some _))) (λ (H : ¬∃ (s : finset M), nonempty (basis ↥s A M)), 1)

source

theorem linear_map.coe_det {M : Type u_2} [add_comm_group M] {A : Type u_5} [comm_ring A] [module A M] [decidable_eq M] :

⇑linear_map.det = dite (∃ (s : finset M), nonempty (basis ↥s A M)) (λ (H : ∃ (s : finset M), nonempty (basis ↥s A M)), ⇑(linear_map.det_aux (trunc.mk (nonempty.some _)))) (λ (H : ¬∃ (s : finset M), nonempty (basis ↥s A M)), 1)

source

theorem linear_map.det_eq_det_to_matrix_of_finset {M : Type u_2} [add_comm_group M] {A : Type u_5} [comm_ring A] [module A M] [decidable_eq M] {s : finset M} (b : basis ↥s A M) (f : M →ₗ[A] M) :

⇑linear_map.det f = (⇑(linear_map.to_matrix b b) f).det

source

@[simp]

theorem linear_map.det_to_matrix {M : Type u_2} [add_comm_group M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [comm_ring A] [module A M] (b : basis ι A M) (f : M →ₗ[A] M) :

(⇑(linear_map.to_matrix b b) f).det = ⇑linear_map.det f

source

@[simp]

theorem linear_map.det_to_matrix' {A : Type u_5} [comm_ring A] {ι : Type u_1} [fintype ι] [decidable_eq ι] (f : (ι → A) →ₗ[A] ι → A) :

(⇑linear_map.to_matrix' f).det = ⇑linear_map.det f

source

@[simp]

theorem linear_map.det_to_lin {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (b : basis ι R M) (f : matrix ι ι R) :

⇑linear_map.det (⇑(matrix.to_lin b b) f) = f.det

source

@[simp]

theorem linear_map.det_to_lin' {R : Type u_1} [comm_ring R] {ι : Type u_4} [decidable_eq ι] [fintype ι] (f : matrix ι ι R) :

⇑linear_map.det (⇑matrix.to_lin' f) = f.det

source

theorem linear_map.det_cases {M : Type u_2} [add_comm_group M] {A : Type u_5} [comm_ring A] [module A M] [decidable_eq M] {P : A → Prop} (f : M →ₗ[A] M) (hb : ∀ (s : finset M) (b : basis ↥s A M), P (⇑(linear_map.to_matrix b b) f).det) (h1 : P 1) :

P (⇑linear_map.det f)

To show P f.det it suffices to consider P (to_matrix _ _ f).det and P 1.

source

@[simp]

theorem linear_map.det_comp {M : Type u_2} [add_comm_group M] {A : Type u_5} [comm_ring A] [module A M] (f g : M →ₗ[A] M) :

⇑linear_map.det (f.comp g) = ⇑linear_map.det f * ⇑linear_map.det g

source

@[simp]

theorem linear_map.det_id {M : Type u_2} [add_comm_group M] {A : Type u_5} [comm_ring A] [module A M] :

⇑linear_map.det linear_map.id = 1

source

@[simp]

theorem linear_map.det_smul {𝕜 : Type u_1} [field 𝕜] {M : Type u_2} [add_comm_group M] [module 𝕜 M] (c : 𝕜) (f : M →ₗ[𝕜] M) :

⇑linear_map.det (c • f) = c ^ finite_dimensional.finrank 𝕜 M * ⇑linear_map.det f

Multiplying a map by a scalar c multiplies its determinant by c ^ dim M.

source

theorem linear_map.det_zero' {M : Type u_2} [add_comm_group M] {A : Type u_5} [comm_ring A] [module A M] {ι : Type u_1} [finite ι] [nonempty ι] (b : basis ι A M) :

⇑linear_map.det 0 = 0

source

@[simp]

theorem linear_map.det_zero {𝕜 : Type u_1} [field 𝕜] {M : Type u_2} [add_comm_group M] [module 𝕜 M] :

⇑linear_map.det 0 = 0 ^ finite_dimensional.finrank 𝕜 M

In a finite-dimensional vector space, the zero map has determinant 1 in dimension 0, and 0 otherwise. We give a formula that also works in infinite dimension, where we define the determinant to be 1.

source

theorem linear_map.det_eq_one_of_subsingleton {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] [subsingleton M] (f : M →ₗ[R] M) :

⇑linear_map.det f = 1

source

theorem linear_map.det_eq_one_of_finrank_eq_zero {𝕜 : Type u_1} [field 𝕜] {M : Type u_2} [add_comm_group M] [module 𝕜 M] (h : finite_dimensional.finrank 𝕜 M = 0) (f : M →ₗ[𝕜] M) :

⇑linear_map.det f = 1

source

@[simp]

theorem linear_map.det_conj {M : Type u_2} [add_comm_group M] {A : Type u_5} [comm_ring A] [module A M] {N : Type u_1} [add_comm_group N] [module A N] (f : M →ₗ[A] M) (e : M ≃ₗ[A] N) :

⇑linear_map.det (↑e.comp (f.comp ↑(e.symm))) = ⇑linear_map.det f

Conjugating a linear map by a linear equiv does not change its determinant.

source

theorem linear_map.is_unit_det {M : Type u_2} [add_comm_group M] {A : Type u_1} [comm_ring A] [module A M] (f : M →ₗ[A] M) (hf : is_unit f) :

is_unit (⇑linear_map.det f)

If a linear map is invertible, so is its determinant.

source

theorem linear_map.finite_dimensional_of_det_ne_one {M : Type u_2} [add_comm_group M] {𝕜 : Type u_1} [field 𝕜] [module 𝕜 M] (f : M →ₗ[𝕜] M) (hf : ⇑linear_map.det f ≠ 1) :

finite_dimensional 𝕜 M

If a linear map has determinant different from 1, then the space is finite-dimensional.

source

theorem linear_map.range_lt_top_of_det_eq_zero {M : Type u_2} [add_comm_group M] {𝕜 : Type u_1} [field 𝕜] [module 𝕜 M] {f : M →ₗ[𝕜] M} (hf : ⇑linear_map.det f = 0) :

linear_map.range f < ⊤

If the determinant of a map vanishes, then the map is not onto.

source

theorem linear_map.bot_lt_ker_of_det_eq_zero {M : Type u_2} [add_comm_group M] {𝕜 : Type u_1} [field 𝕜] [module 𝕜 M] {f : M →ₗ[𝕜] M} (hf : ⇑linear_map.det f = 0) :

⊥ < linear_map.ker f

If the determinant of a map vanishes, then the map is not injective.

source

@[protected]

noncomputable def linear_equiv.det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] :

(M ≃ₗ[R] M) →* Rˣ

On a linear_equiv, the domain of linear_map.det can be promoted to Rˣ.

Equations

linear_equiv.det = (units.map linear_map.det).comp (linear_map.general_linear_group.general_linear_equiv R M).symm.to_monoid_hom

source

@[simp]

theorem linear_equiv.coe_det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (f : M ≃ₗ[R] M) :

↑(⇑linear_equiv.det f) = ⇑linear_map.det ↑f

source

@[simp]

theorem linear_equiv.coe_inv_det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (f : M ≃ₗ[R] M) :

↑(⇑linear_equiv.det f)⁻¹ = ⇑linear_map.det ↑(f.symm)

source

@[simp]

theorem linear_equiv.det_refl {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] :

⇑linear_equiv.det (linear_equiv.refl R M) = 1

source

@[simp]

theorem linear_equiv.det_trans {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (f g : M ≃ₗ[R] M) :

⇑linear_equiv.det (f.trans g) = ⇑linear_equiv.det g * ⇑linear_equiv.det f

source

@[simp]

theorem linear_equiv.det_symm {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (f : M ≃ₗ[R] M) :

⇑linear_equiv.det f.symm = (⇑linear_equiv.det f)⁻¹

source

@[simp]

theorem linear_equiv.det_conj {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {M' : Type u_3} [add_comm_group M'] [module R M'] (f : M ≃ₗ[R] M) (e : M ≃ₗ[R] M') :

⇑linear_equiv.det ((e.symm.trans f).trans e) = ⇑linear_equiv.det f

Conjugating a linear equiv by a linear equiv does not change its determinant.

source

@[simp]

theorem linear_equiv.det_mul_det_symm {M : Type u_2} [add_comm_group M] {A : Type u_1} [comm_ring A] [module A M] (f : M ≃ₗ[A] M) :

⇑linear_map.det ↑f * ⇑linear_map.det ↑(f.symm) = 1

The determinants of a linear_equiv and its inverse multiply to 1.

source

@[simp]

theorem linear_equiv.det_symm_mul_det {M : Type u_2} [add_comm_group M] {A : Type u_1} [comm_ring A] [module A M] (f : M ≃ₗ[A] M) :

⇑linear_map.det ↑(f.symm) * ⇑linear_map.det ↑f = 1

The determinants of a linear_equiv and its inverse multiply to 1.

source

theorem linear_equiv.is_unit_det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {M' : Type u_3} [add_comm_group M'] [module R M'] {ι : Type u_4} [decidable_eq ι] [fintype ι] (f : M ≃ₗ[R] M') (v : basis ι R M) (v' : basis ι R M') :

is_unit (⇑(linear_map.to_matrix v v') ↑f).det

source

theorem linear_equiv.is_unit_det' {M : Type u_2} [add_comm_group M] {A : Type u_1} [comm_ring A] [module A M] (f : M ≃ₗ[A] M) :

is_unit (⇑linear_map.det ↑f)

Specialization of linear_equiv.is_unit_det

source

theorem linear_equiv.det_coe_symm {M : Type u_2} [add_comm_group M] {𝕜 : Type u_1} [field 𝕜] [module 𝕜 M] (f : M ≃ₗ[𝕜] M) :

⇑linear_map.det ↑(f.symm) = (⇑linear_map.det ↑f)⁻¹

The determinant of f.symm is the inverse of that of f when f is a linear equiv.

source

@[simp]

theorem linear_equiv.of_is_unit_det_apply {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {M' : Type u_3} [add_comm_group M'] [module R M'] {ι : Type u_4} [decidable_eq ι] [fintype ι] {f : M →ₗ[R] M'} {v : basis ι R M} {v' : basis ι R M'} (h : is_unit (⇑(linear_map.to_matrix v v') f).det) (ᾰ : M) :

⇑(linear_equiv.of_is_unit_det h) ᾰ = ⇑f ᾰ

source

@[simp]

theorem linear_equiv.of_is_unit_det_symm_apply {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {M' : Type u_3} [add_comm_group M'] [module R M'] {ι : Type u_4} [decidable_eq ι] [fintype ι] {f : M →ₗ[R] M'} {v : basis ι R M} {v' : basis ι R M'} (h : is_unit (⇑(linear_map.to_matrix v v') f).det) (ᾰ : M') :

⇑((linear_equiv.of_is_unit_det h).symm) ᾰ = ⇑(⇑(matrix.to_lin v' v) (⇑(linear_map.to_matrix v v') f)⁻¹) ᾰ

source

noncomputable def linear_equiv.of_is_unit_det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {M' : Type u_3} [add_comm_group M'] [module R M'] {ι : Type u_4} [decidable_eq ι] [fintype ι] {f : M →ₗ[R] M'} {v : basis ι R M} {v' : basis ι R M'} (h : is_unit (⇑(linear_map.to_matrix v v') f).det) :

M ≃ₗ[R] M'

Builds a linear equivalence from a linear map whose determinant in some bases is a unit.

Equations

linear_equiv.of_is_unit_det h = {to_fun := ⇑f, map_add' := _, map_smul' := _, inv_fun := ⇑(⇑(matrix.to_lin v' v) (⇑(linear_map.to_matrix v v') f)⁻¹), left_inv := _, right_inv := _}

source

@[simp]

theorem linear_equiv.coe_of_is_unit_det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {M' : Type u_3} [add_comm_group M'] [module R M'] {ι : Type u_4} [decidable_eq ι] [fintype ι] {f : M →ₗ[R] M'} {v : basis ι R M} {v' : basis ι R M'} (h : is_unit (⇑(linear_map.to_matrix v v') f).det) :

↑(linear_equiv.of_is_unit_det h) = f

source

@[reducible]

noncomputable def linear_map.equiv_of_det_ne_zero {𝕜 : Type u_1} [field 𝕜] {M : Type u_2} [add_comm_group M] [module 𝕜 M] [finite_dimensional 𝕜 M] (f : M →ₗ[𝕜] M) (hf : ⇑linear_map.det f ≠ 0) :

M ≃ₗ[𝕜] M

Builds a linear equivalence from a linear map on a finite-dimensional vector space whose determinant is nonzero.

Equations

f.equiv_of_det_ne_zero hf = have this : is_unit (⇑(linear_map.to_matrix (finite_dimensional.fin_basis 𝕜 M) (finite_dimensional.fin_basis 𝕜 M)) f).det, from _, linear_equiv.of_is_unit_det this

source

theorem linear_map.associated_det_of_eq_comp {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (e : M ≃ₗ[R] M) (f f' : M →ₗ[R] M) (h : ∀ (x : M), ⇑f x = ⇑f' (⇑e x)) :

associated (⇑linear_map.det f) (⇑linear_map.det f')

source

theorem linear_map.associated_det_comp_equiv {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] (f : N →ₗ[R] M) (e e' : M ≃ₗ[R] N) :

associated (⇑linear_map.det (f.comp ↑e)) (⇑linear_map.det (f.comp ↑e'))

source

noncomputable def basis.det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e : basis ι R M) :

alternating_map R M R ι

The determinant of a family of vectors with respect to some basis, as an alternating multilinear map.

Equations

e.det = {to_fun := λ (v : Π (i : ι), (λ (i : ι), M) i), (e.to_matrix v).det, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}

source

theorem basis.det_apply {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e : basis ι R M) (v : ι → M) :

⇑(e.det) v = (e.to_matrix v).det

source

theorem basis.det_self {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e : basis ι R M) :

⇑(e.det) ⇑e = 1

source

@[simp]

theorem basis.det_is_empty {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e : basis ι R M) [is_empty ι] :

e.det = alternating_map.const_of_is_empty R M ι 1

source

theorem basis.det_ne_zero {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e : basis ι R M) [nontrivial R] :

e.det ≠ 0

basis.det is not the zero map.

source

theorem is_basis_iff_det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e : basis ι R M) {v : ι → M} :

linear_independent R v ∧ submodule.span R (set.range v) = ⊤ ↔ is_unit (⇑(e.det) v)

source

theorem basis.is_unit_det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e e' : basis ι R M) :

is_unit (⇑(e.det) ⇑e')

source

theorem alternating_map.eq_smul_basis_det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e : basis ι R M) (f : alternating_map R M R ι) :

f = ⇑f ⇑e • e.det

Any alternating map to R where ι has the cardinality of a basis equals the determinant map with respect to that basis, multiplied by the value of that alternating map on that basis.

source

@[simp]

theorem alternating_map.map_basis_eq_zero_iff {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [finite ι] (e : basis ι R M) (f : alternating_map R M R ι) :

⇑f ⇑e = 0 ↔ f = 0

source

theorem alternating_map.map_basis_ne_zero_iff {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_3} [finite ι] (e : basis ι R M) (f : alternating_map R M R ι) :

⇑f ⇑e ≠ 0 ↔ f ≠ 0

source

@[simp]

theorem basis.det_comp {M : Type u_2} [add_comm_group M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [comm_ring A] [module A M] (e : basis ι A M) (f : M →ₗ[A] M) (v : ι → M) :

⇑(e.det) (⇑f ∘ v) = ⇑linear_map.det f * ⇑(e.det) v

source

@[simp]

theorem basis.det_comp_basis {M : Type u_2} [add_comm_group M] {M' : Type u_3} [add_comm_group M'] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [comm_ring A] [module A M] [module A M'] (b : basis ι A M) (b' : basis ι A M') (f : M →ₗ[A] M') :

⇑(b'.det) (⇑f ∘ ⇑b) = ⇑linear_map.det (f.comp ↑(b'.equiv b (equiv.refl ι)))

source

theorem basis.det_reindex {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {ι' : Type u_3} [fintype ι'] [decidable_eq ι'] (b : basis ι R M) (v : ι' → M) (e : ι ≃ ι') :

⇑((b.reindex e).det) v = ⇑(b.det) (v ∘ ⇑e)

source

theorem basis.det_reindex_symm {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {ι' : Type u_3} [fintype ι'] [decidable_eq ι'] (b : basis ι R M) (v : ι → M) (e : ι' ≃ ι) :

⇑((b.reindex e.symm).det) (v ∘ ⇑e) = ⇑(b.det) v

source

@[simp]

theorem basis.det_map {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {M' : Type u_3} [add_comm_group M'] [module R M'] {ι : Type u_4} [decidable_eq ι] [fintype ι] (b : basis ι R M) (f : M ≃ₗ[R] M') (v : ι → M') :

⇑((b.map f).det) v = ⇑(b.det) (⇑(f.symm) ∘ v)

source

theorem basis.det_map' {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {M' : Type u_3} [add_comm_group M'] [module R M'] {ι : Type u_4} [decidable_eq ι] [fintype ι] (b : basis ι R M) (f : M ≃ₗ[R] M') :

(b.map f).det = b.det.comp_linear_map ↑(f.symm)

source

@[simp]

theorem pi.basis_fun_det {R : Type u_1} [comm_ring R] {ι : Type u_4} [decidable_eq ι] [fintype ι] :

(pi.basis_fun R ι).det = matrix.det_row_alternating

source

theorem basis.det_smul_mk_coord_eq_det_update {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e : basis ι R M) {v : ι → M} (hli : linear_independent R v) (hsp : ⊤ ≤ submodule.span R (set.range v)) (i : ι) :

⇑(e.det) v • (basis.mk hli hsp).coord i = e.det.to_multilinear_map.to_linear_map v i

If we fix a background basis e, then for any other basis v, we can characterise the coordinates provided by v in terms of determinants relative to e.

source

theorem basis.det_units_smul {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e : basis ι R M) (w : ι → Rˣ) :

(e.units_smul w).det = ↑(finset.univ.prod (λ (i : ι), w i))⁻¹ • e.det

If a basis is multiplied columnwise by scalars w : ι → Rˣ, then the determinant with respect to this basis is multiplied by the product of the inverse of these scalars.

source

@[simp]

theorem basis.det_units_smul_self {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e : basis ι R M) (w : ι → Rˣ) :

⇑(e.det) ⇑(e.units_smul w) = finset.univ.prod (λ (i : ι), ↑(w i))

The determinant of a basis constructed by units_smul is the product of the given units.

source

@[simp]

theorem basis.det_is_unit_smul {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] (e : basis ι R M) {w : ι → R} (hw : ∀ (i : ι), is_unit (w i)) :

⇑(e.det) ⇑(e.is_unit_smul hw) = finset.univ.prod (λ (i : ι), w i)

The determinant of a basis constructed by is_unit_smul is the product of the given units.

mathlib documentation

Determinant of families of vectors #

Main definitions #

Tags #

Determinant of a linear map #