Determinant of families of vectors

This file defines the determinant of an endomorphism, and of a family of vectors with respect to some basis. For the determinant of a matrix, see the file LinearAlgebra.Matrix.Determinant.

Main definitions

In the list below, and in all this file, R is a commutative ring (semiring is sometimes enough), M and its variations are R-modules, ι, κ, n and m are finite types used for indexing.

• Basis.det: the determinant of a family of vectors with respect to a basis, as a multilinear map
• LinearMap.det: the determinant of an endomorphism f : End R M as a multiplicative homomorphism (if M does not have a finite R-basis, the result is 1 instead)
• LinearEquiv.det: the determinant of an isomorphism f : M ≃ₗ[R] M as a multiplicative homomorphism (if M does not have a finite R-basis, the result is 1 instead)

Tags

basis, det, determinant

def equivOfPiLEquivPi {m : Type u_6} {n : Type u_7} {R : Type u_8} [Finite m] [Finite n] [CommRing 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

• equivOfPiLEquivPi e = (Basis.ofEquivFun e.symm).indexEquiv (Pi.basisFun R n)

def Matrix.indexEquivOfInv {A : Type u_5} [CommRing A] {m : Type u_6} {n : Type u_7} [Fintype m] [Fintype n] [Nontrivial A] [DecidableEq m] [DecidableEq n] {M : Matrix m n A} {M' : Matrix n m A} (hMM' : M * M' = 1) (hM'M : M' * 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.indexEquivOfInv hMM' hM'M = equivOfPiLEquivPi (Matrix.toLin'OfInv hMM' hM'M)

theorem Matrix.det_comm {A : Type u_5} [CommRing A] {n : Type u_7} [Fintype n] [DecidableEq n] (M N : Matrix n n A) : (M * N).det = (N * M).det

theorem Matrix.det_comm' {A : Type u_5} [CommRing A] {m : Type u_6} {n : Type u_7} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] {M : Matrix n m A} {N M' : Matrix m n A} (hMM' : M * M' = 1) (hM'M : M' * M = 1) : (M * N).det = (N * M).det

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

theorem Matrix.det_conj_of_mul_eq_one {A : Type u_5} [CommRing A] {m : Type u_6} {n : Type u_7} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] {M : Matrix m n A} {M' : Matrix n m A} {N : Matrix n n A} (hMM' : M * M' = 1) (hM'M : M' * M = 1) : (M * N * 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.

Determinant of a linear map

theorem LinearMap.det_toMatrix_eq_det_toMatrix {M : Type u_2} [AddCommGroup M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {A : Type u_5} [CommRing A] [Module A M] {κ : Type u_6} [Fintype κ] [DecidableEq κ] (b : Basis ι A M) (c : Basis κ A M) (f : M →ₗ[A] M) : ((LinearMap.toMatrix b b) f).det = ((LinearMap.toMatrix c c) f).det

The determinant of LinearMap.toMatrix does not depend on the choice of basis.

theorem LinearMap.detAux_def {M : Type u_7} [AddCommGroup M] {ι : Type u_8} [DecidableEq ι] [Fintype ι] {A : Type u_9} [CommRing A] [Module A M] : LinearMap.detAux = Trunc.lift (fun (b : Basis ι A M) => Matrix.detMonoidHom.comp ↑(LinearMap.toMatrixAlgEquiv b)) ⋯

@[irreducible]

def LinearMap.detAux {M : Type u_7} [AddCommGroup M] {ι : Type u_8} [DecidableEq ι] [Fintype ι] {A : Type u_9} [CommRing A] [Module A M] : Trunc (Basis ι A M) → (M →ₗ[A] M) →* A

The determinant of an endomorphism given a basis.

See LinearMap.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 detAux's type that it does not depend on the choice of basis. Instead you can use the detAux_def'' lemma, or avoid mentioning a basis at all using LinearMap.det.

Equations

• LinearMap.detAux = Trunc.lift (fun (b : Basis ι A M) => Matrix.detMonoidHom.comp ↑(LinearMap.toMatrixAlgEquiv b)) ⋯

theorem LinearMap.detAux_def' {M : Type u_2} [AddCommGroup M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {A : Type u_5} [CommRing A] [Module A M] (b : Basis ι A M) (f : M →ₗ[A] M) : (LinearMap.detAux (Trunc.mk b)) f = ((LinearMap.toMatrix b b) f).det

Unfold lemma for detAux.

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

theorem LinearMap.detAux_def'' {M : Type u_2} [AddCommGroup M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {A : Type u_5} [CommRing A] [Module A M] {ι' : Type u_7} [Fintype ι'] [DecidableEq ι'] (tb : Trunc (Basis ι A M)) (b' : Basis ι' A M) (f : M →ₗ[A] M) : (LinearMap.detAux tb) f = ((LinearMap.toMatrix b' b') f).det

@[simp]

theorem LinearMap.detAux_id {M : Type u_2} [AddCommGroup M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {A : Type u_5} [CommRing A] [Module A M] (b : Trunc (Basis ι A M)) : (LinearMap.detAux b) LinearMap.id = 1

@[simp]

theorem LinearMap.detAux_comp {M : Type u_2} [AddCommGroup M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {A : Type u_5} [CommRing A] [Module A M] (b : Trunc (Basis ι A M)) (f g : M →ₗ[A] M) : (LinearMap.detAux b) (f ∘ₗ g) = (LinearMap.detAux b) f * (LinearMap.detAux b) g

@[irreducible]

def LinearMap.det {M : Type u_7} [AddCommGroup M] {A : Type u_8} [CommRing 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

• LinearMap.det = if H : ∃ (s : Finset M), Nonempty (Basis { x : M // x ∈ s } A M) then LinearMap.detAux (Trunc.mk ⋯.some) else 1

theorem LinearMap.det_def {M : Type u_7} [AddCommGroup M] {A : Type u_8} [CommRing A] [Module A M] : LinearMap.det = if H : ∃ (s : Finset M), Nonempty (Basis { x : M // x ∈ s } A M) then LinearMap.detAux (Trunc.mk ⋯.some) else 1

theorem LinearMap.coe_det {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] [DecidableEq M] : ⇑LinearMap.det = ⇑(if H : ∃ (s : Finset M), Nonempty (Basis { x : M // x ∈ s } A M) then LinearMap.detAux (Trunc.mk ⋯.some) else 1)

theorem LinearMap.det_eq_det_toMatrix_of_finset {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] [DecidableEq M] {s : Finset M} (b : Basis { x : M // x ∈ s } A M) (f : M →ₗ[A] M) : LinearMap.det f = ((LinearMap.toMatrix b b) f).det

@[simp]

theorem LinearMap.det_toMatrix {M : Type u_2} [AddCommGroup M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {A : Type u_5} [CommRing A] [Module A M] (b : Basis ι A M) (f : M →ₗ[A] M) : ((LinearMap.toMatrix b b) f).det = LinearMap.det f

@[simp]

theorem LinearMap.det_toMatrix' {A : Type u_5} [CommRing A] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (f : (ι → A) →ₗ[A] ι → A) : (LinearMap.toMatrix' f).det = LinearMap.det f

@[simp]

theorem LinearMap.det_toLin {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (f : Matrix ι ι R) : LinearMap.det ((Matrix.toLin b b) f) = f.det

@[simp]

theorem LinearMap.det_toLin' {R : Type u_1} [CommRing R] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (f : Matrix ι ι R) : LinearMap.det (Matrix.toLin' f) = f.det

theorem LinearMap.det_cases {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] [DecidableEq M] {P : A → Prop} (f : M →ₗ[A] M) (hb : ∀ (s : Finset M) (b : Basis { x : M // x ∈ s } A M), P ((LinearMap.toMatrix b b) f).det) (h1 : P 1) : P (LinearMap.det f)

To show P (LinearMap.det f) it suffices to consider P (Matrix.det (toMatrix _ _ f)) and P 1.

@[simp]

theorem LinearMap.det_comp {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] (f g : M →ₗ[A] M) : LinearMap.det (f ∘ₗ g) = LinearMap.det f * LinearMap.det g

@[simp]

theorem LinearMap.det_id {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] : LinearMap.det LinearMap.id = 1

@[simp]

theorem LinearMap.det_smul {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] [Module.Free A M] (c : A) (f : M →ₗ[A] M) : LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

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

theorem LinearMap.det_zero' {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] {ι : Type u_7} [Finite ι] [Nonempty ι] (b : Basis ι A M) : LinearMap.det 0 = 0

@[simp]

theorem LinearMap.det_zero {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] [Module.Free A M] : LinearMap.det 0 = 0 ^ Module.finrank A 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.

theorem LinearMap.det_eq_one_of_not_module_finite {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (h : ¬Module.Finite R M) (f : M →ₗ[R] M) : LinearMap.det f = 1

theorem LinearMap.det_eq_one_of_subsingleton {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Subsingleton M] (f : M →ₗ[R] M) : LinearMap.det f = 1

theorem LinearMap.det_eq_one_of_finrank_eq_zero {𝕜 : Type u_7} [Field 𝕜] {M : Type u_8} [AddCommGroup M] [Module 𝕜 M] (h : Module.finrank 𝕜 M = 0) (f : M →ₗ[𝕜] M) : LinearMap.det f = 1

@[simp]

theorem LinearMap.det_conj {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] {N : Type u_7} [AddCommGroup N] [Module A N] (f : M →ₗ[A] M) (e : M ≃ₗ[A] N) : LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

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

theorem LinearMap.isUnit_det {M : Type u_2} [AddCommGroup M] {A : Type u_7} [CommRing A] [Module A M] (f : M →ₗ[A] M) (hf : IsUnit f) : IsUnit (LinearMap.det f)

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

theorem LinearMap.finiteDimensional_of_det_ne_one {M : Type u_2} [AddCommGroup M] {𝕜 : Type u_7} [Field 𝕜] [Module 𝕜 M] (f : M →ₗ[𝕜] M) (hf : LinearMap.det f ≠ 1) : FiniteDimensional 𝕜 M

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

theorem LinearMap.range_lt_top_of_det_eq_zero {M : Type u_2} [AddCommGroup M] {𝕜 : Type u_7} [Field 𝕜] [Module 𝕜 M] {f : M →ₗ[𝕜] M} (hf : LinearMap.det f = 0) : LinearMap.range f < ⊤

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

theorem LinearMap.bot_lt_ker_of_det_eq_zero {M : Type u_2} [AddCommGroup M] {𝕜 : Type u_7} [Field 𝕜] [Module 𝕜 M] {f : M →ₗ[𝕜] M} (hf : LinearMap.det f = 0) : ⊥ < LinearMap.ker f

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

@[simp]

theorem LinearMap.det_ring {R : Type u_1} [CommRing R] (f : R →ₗ[R] R) : LinearMap.det f = f 1

When the function is over the base ring, the determinant is the evaluation at 1.

theorem LinearMap.det_mulLeft {R : Type u_1} [CommRing R] (a : R) : LinearMap.det (LinearMap.mulLeft R a) = a

theorem LinearMap.det_mulRight {R : Type u_1} [CommRing R] (a : R) : LinearMap.det (LinearMap.mulRight R a) = a

@[irreducible]

def LinearEquiv.det {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] : (M ≃ₗ[R] M) →* Rˣ

On a LinearEquiv, the domain of LinearMap.det can be promoted to Rˣ.

Equations

• LinearEquiv.det = (Units.map LinearMap.det).comp (LinearMap.GeneralLinearGroup.generalLinearEquiv R M).symm.toMonoidHom

@[simp]

theorem LinearEquiv.coe_det {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (f : M ≃ₗ[R] M) : ↑(LinearEquiv.det f) = LinearMap.det ↑f

@[simp]

theorem LinearEquiv.coe_inv_det {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (f : M ≃ₗ[R] M) : ↑(LinearEquiv.det f)⁻¹ = LinearMap.det ↑f.symm

@[simp]

theorem LinearEquiv.det_refl {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] : LinearEquiv.det (LinearEquiv.refl R M) = 1

@[simp]

theorem LinearEquiv.det_trans {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (f g : M ≃ₗ[R] M) : LinearEquiv.det (f ≪≫ₗ g) = LinearEquiv.det g * LinearEquiv.det f

@[simp]

theorem LinearEquiv.det_symm {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (f : M ≃ₗ[R] M) : LinearEquiv.det f.symm = LinearEquiv.det f⁻¹

@[simp]

theorem LinearEquiv.det_conj {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (f : M ≃ₗ[R] M) (e : M ≃ₗ[R] M') : LinearEquiv.det (e.symm ≪≫ₗ f ≪≫ₗ e) = LinearEquiv.det f

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

@[simp]

theorem LinearEquiv.det_mul_det_symm {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) : LinearMap.det ↑f * LinearMap.det ↑f.symm = 1

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

@[simp]

theorem LinearEquiv.det_symm_mul_det {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) : LinearMap.det ↑f.symm * LinearMap.det ↑f = 1

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

theorem LinearEquiv.isUnit_det {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (f : M ≃ₗ[R] M') (v : Basis ι R M) (v' : Basis ι R M') : IsUnit ((LinearMap.toMatrix v v') ↑f).det

theorem LinearEquiv.isUnit_det' {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) : IsUnit (LinearMap.det ↑f)

Specialization of LinearEquiv.isUnit_det

theorem LinearEquiv.det_coe_symm {M : Type u_2} [AddCommGroup M] {𝕜 : Type u_5} [Field 𝕜] [Module 𝕜 M] (f : M ≃ₗ[𝕜] M) : LinearMap.det ↑f.symm = (LinearMap.det ↑f)⁻¹

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

def LinearEquiv.ofIsUnitDet {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {f : M →ₗ[R] M'} {v : Basis ι R M} {v' : Basis ι R M'} (h : IsUnit ((LinearMap.toMatrix v v') f).det) : M ≃ₗ[R] M'

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

Equations

• LinearEquiv.ofIsUnitDet h = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑((Matrix.toLin v' v) ((LinearMap.toMatrix v v') f)⁻¹), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearEquiv.ofIsUnitDet_symm_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {f : M →ₗ[R] M'} {v : Basis ι R M} {v' : Basis ι R M'} (h : IsUnit ((LinearMap.toMatrix v v') f).det) (a : M') : (LinearEquiv.ofIsUnitDet h).symm a = ((Matrix.toLin v' v) ((LinearMap.toMatrix v v') f)⁻¹) a

@[simp]

theorem LinearEquiv.ofIsUnitDet_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {f : M →ₗ[R] M'} {v : Basis ι R M} {v' : Basis ι R M'} (h : IsUnit ((LinearMap.toMatrix v v') f).det) (a : M) : (LinearEquiv.ofIsUnitDet h) a = f a

@[simp]

theorem LinearEquiv.coe_ofIsUnitDet {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {f : M →ₗ[R] M'} {v : Basis ι R M} {v' : Basis ι R M'} (h : IsUnit ((LinearMap.toMatrix v v') f).det) : ↑(LinearEquiv.ofIsUnitDet h) = f

@[reducible, inline]

abbrev LinearMap.equivOfDetNeZero {𝕜 : Type u_5} [Field 𝕜] {M : Type u_6} [AddCommGroup M] [Module 𝕜 M] [FiniteDimensional 𝕜 M] (f : M →ₗ[𝕜] M) (hf : LinearMap.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.equivOfDetNeZero hf = LinearEquiv.ofIsUnitDet ⋯

theorem LinearMap.associated_det_of_eq_comp {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (e : M ≃ₗ[R] M) (f f' : M →ₗ[R] M) (h : ∀ (x : M), f x = f' (e x)) : Associated (LinearMap.det f) (LinearMap.det f')

theorem LinearMap.associated_det_comp_equiv {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (f : N →ₗ[R] M) (e e' : M ≃ₗ[R] N) : Associated (LinearMap.det (f ∘ₗ ↑e)) (LinearMap.det (f ∘ₗ ↑e'))

def Basis.det {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) : M [⋀^ι]→ₗ[R] R

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

Equations

• e.det = { toFun := fun (v : ι → M) => (e.toMatrix v).det, map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ }

theorem Basis.det_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) (v : ι → M) : e.det v = (e.toMatrix v).det

theorem Basis.det_self {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) : e.det ⇑e = 1

@[simp]

theorem Basis.det_isEmpty {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) [IsEmpty ι] : e.det = AlternatingMap.constOfIsEmpty R M ι 1

theorem Basis.det_ne_zero {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) [Nontrivial R] : e.det ≠ 0

Basis.det is not the zero map.

theorem Basis.smul_det {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) {G : Type u_5} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) (v : ι → M) : (g • e).det v = e.det (g⁻¹ • v)

theorem is_basis_iff_det {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) {v : ι → M} : LinearIndependent R v ∧ Submodule.span R (Set.range v) = ⊤ ↔ IsUnit (e.det v)

theorem Basis.isUnit_det {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e e' : Basis ι R M) : IsUnit (e.det ⇑e')

theorem AlternatingMap.eq_smul_basis_det {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) (f : M [⋀^ι]→ₗ[R] 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.

@[simp]

theorem AlternatingMap.map_basis_eq_zero_iff {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_5} [Finite ι] (e : Basis ι R M) (f : M [⋀^ι]→ₗ[R] R) : f ⇑e = 0 ↔ f = 0

theorem AlternatingMap.map_basis_ne_zero_iff {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_5} [Finite ι] (e : Basis ι R M) (f : M [⋀^ι]→ₗ[R] R) : f ⇑e ≠ 0 ↔ f ≠ 0

@[simp]

theorem Basis.det_comp {M : Type u_2} [AddCommGroup M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {A : Type u_5} [CommRing A] [Module A M] (e : Basis ι A M) (f : M →ₗ[A] M) (v : ι → M) : e.det (⇑f ∘ v) = LinearMap.det f * e.det v

@[simp]

theorem Basis.det_comp_basis {M : Type u_2} [AddCommGroup M] {M' : Type u_3} [AddCommGroup M'] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {A : Type u_5} [CommRing A] [Module A M] [Module A M'] (b : Basis ι A M) (b' : Basis ι A M') (f : M →ₗ[A] M') : b'.det (⇑f ∘ ⇑b) = LinearMap.det (f ∘ₗ ↑(b'.equiv b (Equiv.refl ι)))

@[simp]

theorem Basis.det_basis {M : Type u_2} [AddCommGroup M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {A : Type u_5} [CommRing A] [Module A M] (b b' : Basis ι A M) : LinearMap.det ↑(b'.equiv b (Equiv.refl ι)) = b'.det ⇑b

theorem Basis.det_inv {M : Type u_2} [AddCommGroup M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {A : Type u_5} [CommRing A] [Module A M] (b b' : Basis ι A M) : ↑⋯.unit⁻¹ = b'.det ⇑b

theorem Basis.det_reindex {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {ι' : Type u_6} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι') : (b.reindex e).det v = b.det (v ∘ ⇑e)

theorem Basis.det_reindex' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {ι' : Type u_6} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (e : ι ≃ ι') : (b.reindex e).det = AlternatingMap.domDomCongr e b.det

theorem Basis.det_reindex_symm {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {ι' : Type u_6} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (v : ι → M) (e : ι' ≃ ι) : (b.reindex e.symm).det (v ∘ ⇑e) = b.det v

@[simp]

theorem Basis.det_map {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (f : M ≃ₗ[R] M') (v : ι → M') : (b.map f).det v = b.det (⇑f.symm ∘ v)

theorem Basis.det_map' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (f : M ≃ₗ[R] M') : (b.map f).det = b.det.compLinearMap ↑f.symm

@[simp]

theorem Pi.basisFun_det {R : Type u_1} [CommRing R] {ι : Type u_4} [DecidableEq ι] [Fintype ι] : (Pi.basisFun R ι).det = Matrix.detRowAlternating

theorem Pi.basisFun_det_apply {R : Type u_1} [CommRing R] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (v : ι → ι → R) : (Pi.basisFun R ι).det v = (Matrix.of v).det

theorem Basis.det_smul_mk_coord_eq_det_update {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) {v : ι → M} (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) (i : ι) : e.det v • (Basis.mk hli hsp).coord i = (↑e.det).toLinearMap 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.

theorem Basis.det_unitsSMul {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) (w : ι → Rˣ) : (e.unitsSMul w).det = ↑(∏ 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.

@[simp]

theorem Basis.det_unitsSMul_self {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) (w : ι → Rˣ) : e.det ⇑(e.unitsSMul w) = ∏ i : ι, ↑(w i)

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

@[simp]

theorem Basis.det_isUnitSMul {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Basis ι R M) {w : ι → R} (hw : ∀ (i : ι), IsUnit (w i)) : e.det ⇑(e.isUnitSMul hw) = ∏ i : ι, w i

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