# 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

source
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 = (Module.Basis.ofEquivFun e.symm).indexEquiv (Pi.basisFun R n)

Instances For

source
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)

Instances For

source
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
source
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)`.

source
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 #

source
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 : Module.Basis ι A M) (c : Module.Basis κ A M) (f : M →ₗ[A] M) :
((toMatrix b b) f).det = ((toMatrix c c) f).det

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

source
@[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 (Module.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 : Module.Basis ι A M) => Matrix.detMonoidHom.comp ↑(LinearMap.toMatrixAlgEquiv b)) ⋯

Instances For

source
theorem LinearMap.detAux_def {M : Type u_7} [AddCommGroup M] {ι : Type u_8} [DecidableEq ι] [Fintype ι] {A : Type u_9} [CommRing A] [Module A M] :
detAux = Trunc.lift (fun (b : Module.Basis ι A M) => Matrix.detMonoidHom.comp ↑(toMatrixAlgEquiv b)) ⋯
source
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 : Module.Basis ι A M) (f : M →ₗ[A] M) :
(detAux (Trunc.mk b)) f = ((toMatrix b b) f).det

Unfold lemma for `detAux`.

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

source
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 (Module.Basis ι A M)) (b' : Module.Basis ι' A M) (f : M →ₗ[A] M) :
(detAux tb) f = ((toMatrix b' b') f).det
source
@[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 (Module.Basis ι A M)) :
(detAux b) id = 1
source
@[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 (Module.Basis ι A M)) (f g : M →ₗ[A] M) :
(detAux b) (f ∘ₗ g) = (detAux b) f * (detAux b) g
source
@[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 (Module.Basis (↥s) A M) then LinearMap.detAux (Trunc.mk ⋯.some) else 1

Instances For

source
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 (Module.Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1
source
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 (Module.Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1)
source
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 : Module.Basis (↥s) A M) (f : M →ₗ[A] M) :
LinearMap.det f = ((toMatrix b b) f).det
source
@[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 : Module.Basis ι A M) (f : M →ₗ[A] M) :
((toMatrix b b) f).det = LinearMap.det f
source
@[simp]
theorem LinearMap.det_toMatrix' {A : Type u_5} [CommRing A] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (f : (ι → A) →ₗ[A] ι → A) :
(toMatrix' f).det = LinearMap.det f
source
@[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 : Module.Basis ι R M) (f : Matrix ι ι R) :
LinearMap.det ((Matrix.toLin b b) f) = f.det
source
@[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
source
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 : Module.Basis (↥s) A M), P ((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`.

source
@[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
source
@[simp]
theorem LinearMap.det_id {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A] [Module A M] :
LinearMap.det id = 1
source
@[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`.

source
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 : Module.Basis ι A M) :
LinearMap.det 0 = 0
source
@[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`.

source
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
source
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
source
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
source
@[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.

source
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.

source
theorem LinearMap.isUnit_iff_isUnit_det {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] (f : M →ₗ[R] M) :
IsUnit f ↔ IsUnit (LinearMap.det f)
source
theorem LinearMap.finite_of_det_ne_one {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {f : M →ₗ[R] M} (hf : LinearMap.det f ≠ 1) :
Module.Finite R M

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

source
@[deprecated "use `finite_of_det_ne_one` instead" (since := "2025-09-15")]
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
source
theorem LinearMap.bot_lt_ker_of_det_eq_zero {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsDomain R] [Module.Free R M] {f : M →ₗ[R] M} (hf : LinearMap.det f = 0) :
⊥ < ker f

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

source
theorem LinearMap.det_eq_zero_iff_ker_ne_bot {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsDomain R] [Module.Free R M] [Module.Finite R M] {f : M →ₗ[R] M} :
LinearMap.det f = 0 ↔ ker f ≠ ⊥

The determinant of a map vanishes iff the map is not injective.

source
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) :
range f < ⊤

If the determinant of a map vanishes, then the map is not onto. TODO: This should only require `[IsDomain R] [Free R M]`, which we get if we generalize `Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean`, which includes `LinearMap.ker_eq_bot_iff_range_eq_top`.

source
@[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`.

source
theorem LinearMap.det_mulLeft {R : Type u_1} [CommRing R] (a : R) :
LinearMap.det (mulLeft R a) = a
source
theorem LinearMap.det_mulRight {R : Type u_1} [CommRing R] (a : R) :
LinearMap.det (mulRight R a) = a
source
theorem LinearMap.det_prodMap {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] [Module.Free R M] [Module.Free R M'] [Module.Finite R M] [Module.Finite R M'] (f : Module.End R M) (f' : Module.End R M') :
LinearMap.det (prodMap f f') = LinearMap.det f * LinearMap.det f'
source
theorem LinearMap.det_pi {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [Fintype ι] [Module.Free R M] [Module.Finite R M] (f : ι → M →ₗ[R] M) :
LinearMap.det (pi fun (i : ι) => f i ∘ₗ proj i) = ∏ i : ι, LinearMap.det (f i)
source
@[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

Instances For

source
@[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
source
@[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
source
@[simp]
theorem LinearEquiv.det_refl {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] :
LinearEquiv.det (refl R M) = 1
source
@[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
source
@[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⁻¹
source
@[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.

source
@[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.

source
@[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.

source
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 : Module.Basis ι R M) (v' : Module.Basis ι R M') :
IsUnit ((LinearMap.toMatrix v v') ↑f).det
source
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`

source
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.

source
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 : Module.Basis ι R M} {v' : Module.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 := ⋯ }

Instances For

source
@[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 : Module.Basis ι R M} {v' : Module.Basis ι R M'} (h : IsUnit ((LinearMap.toMatrix v v') f).det) (a : M) :
(ofIsUnitDet h) a = f a
source
@[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 : Module.Basis ι R M} {v' : Module.Basis ι R M'} (h : IsUnit ((LinearMap.toMatrix v v') f).det) (a : M') :
(ofIsUnitDet h).symm a = ((Matrix.toLin v' v) ((LinearMap.toMatrix v v') f)⁻¹) a
source
@[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 : Module.Basis ι R M} {v' : Module.Basis ι R M'} (h : IsUnit ((LinearMap.toMatrix v v') f).det) :
↑(ofIsUnitDet h) = f
source
noncomputable def LinearMap.equivOfIsUnitDet {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {f : M →ₗ[R] M} (h : IsUnit (LinearMap.det f)) :
M ≃ₗ[R] M

Builds a linear equivalence from an endomorphism whose determinant is a unit.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem LinearMap.equivOfIsUnitDet_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {f : M →ₗ[R] M} (h : IsUnit (LinearMap.det f)) (x : M) :
(equivOfIsUnitDet h) x = f x
source
@[simp]
theorem LinearMap.coe_equivOfIsUnitDet {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {f : M →ₗ[R] M} (h : IsUnit (LinearMap.det f)) :
↑(equivOfIsUnitDet h) = f
source
@[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 ⋯

Instances For

source
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')
source
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'))
source
def Module.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 = { toMultilinearMap := MultilinearMap.mk' (fun (v : ι → M) => (e.toMatrix v).det) ⋯ ⋯, map_eq_zero_of_eq' := ⋯ }

Instances For

source
theorem Module.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
source
theorem Module.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
source
@[simp]
theorem Module.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
source
theorem Module.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.

source
theorem Module.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)
source
theorem Module.Basis.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)
source
theorem Module.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')
source
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 : Module.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.

source
@[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 : Module.Basis ι R M) (f : M [⋀^ι]→ₗ[R] R) :
f ⇑e = 0 ↔ f = 0
source
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 : Module.Basis ι R M) (f : M [⋀^ι]→ₗ[R] R) :
f ⇑e ≠ 0 ↔ f ≠ 0
source
@[simp]
theorem Module.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
source
@[simp]
theorem Module.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 ι)))
source
@[simp]
theorem Module.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
source
theorem Module.Basis.det_mul_det {M : Type u_2} [AddCommGroup M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {A : Type u_5} [CommRing A] [Module A M] (b b' b'' : Basis ι A M) :
b.det ⇑b' * b'.det ⇑b'' = b.det ⇑b''
source
theorem Module.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
source
theorem Module.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)
source
theorem Module.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
source
theorem Module.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
source
@[simp]
theorem Module.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)
source
theorem Module.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
source
@[simp]
theorem Pi.basisFun_det {R : Type u_1} [CommRing R] {ι : Type u_4} [DecidableEq ι] [Fintype ι] :
(basisFun R ι).det = Matrix.detRowAlternating
source
theorem Pi.basisFun_det_apply {R : Type u_1} [CommRing R] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (v : ι → ι → R) :
(basisFun R ι).det v = (Matrix.of v).det
source
theorem Module.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`.

source
theorem Module.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.

source
@[simp]
theorem Module.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.

source
@[simp]
theorem Module.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.

source
theorem LinearMap.det_dualMap {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) :
LinearMap.det f.dualMap = LinearMap.det f

The determinant of the transpose of an endomorphism coincides with its determinant.