LinearMap.det_toMatrix_eq_det_toMatrix
theorem LinearMap.det_toMatrix_eq_det_toMatrix :
∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
[inst_3 : CommRing A] [inst_4 : Module A M] {κ : Type u_6} [inst_5 : Fintype κ] [inst_6 : 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
This theorem states that the determinant of a linear map, when converted to a matrix representation using `LinearMap.toMatrix`, does not depend on the choice of basis. Given two bases `b` and `c` over a certain module `M`, of an arbitrary commutative ring `A`, and a linear map `f` from `M` to `M`, the determinant of the matrix representation of `f` with respect to basis `b` is equal to the determinant of the matrix representation of `f` with respect to basis `c`. This holds for all types `M`, `ι`, `A`, `κ` where `M` is an additively commutative group, both `ι` and `κ` are types with decidable equality and finite, and `A` is a commutative ring which is also a module over `M`.
More concisely: For any commutative ring A, module M with decidable equality and finite types ι and κ, and for any linear map f from M to M and bases b and c of M, the determinant of the matrix representation of f with respect to basis b is equal to the determinant of the matrix representation of f with respect to basis c.
|
Basis.det_smul_mk_coord_eq_det_update
theorem Basis.det_smul_mk_coord_eq_det_update :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
[inst_3 : DecidableEq ι] [inst_4 : 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
This theorem states that given a commutative ring `R` and a module `M` over `R` with a fixed background basis `e`, for any other basis `v` of `M` which is linearly independent and spans the module, we can express the coordinates given by `v` in terms of determinants relative to the background basis `e`. More specifically, the determinant of `v` with respect to `e` scaled by the coordinates given by `v` for any vector `i` is equivalent to the i-th coordinate of the vector transformation of `v` by the determinant of `e`.
More concisely: Given a commutative ring `R`, an `R`-module `M` with a fixed basis `e`, and any linearly independent basis `v` of `M` that spans it, the determinant of the change of basis matrix from `v` to `e`, scaled by the coordinates of `i` in `v`, is equal to the `i`-th coordinate of the vector obtained by applying the determinant of `e` to `i` as a column vector.
|
LinearEquiv.det_coe_symm
theorem LinearEquiv.det_coe_symm :
∀ {M : Type u_2} [inst : AddCommGroup M] {𝕜 : Type u_5} [inst_1 : Field 𝕜] [inst_2 : Module 𝕜 M] (f : M ≃ₗ[𝕜] M),
LinearMap.det ↑f.symm = (LinearMap.det ↑f)⁻¹
This theorem states that for any linear equivalence `f` from a module `M` to itself over a field `𝕜`, the determinant of the inverse of `f` (denoted by `f.symm`) equals the inverse of the determinant of `f`. Here, `M` is a type with an additional structure of an additive commutative group, and `𝕜` is a type with a field structure. The determinant is computed in a way that does not depend on the choice of a basis for `M`. If `M` has no finite basis, the determinant is defined as `1`.
More concisely: For any linear endomorphism `f` of a module `M` over a field `𝕜`, the determinant of `f.symm` equals the multiplicative inverse of the determinant of `f`.
|
LinearMap.isUnit_det
theorem LinearMap.isUnit_det :
∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_7} [inst_1 : CommRing A] [inst_2 : Module A M] (f : M →ₗ[A] M),
IsUnit f → IsUnit (LinearMap.det f)
This theorem states that if a linear map `f` from a module `M` to itself over a commutative ring `A` is a unit (meaning it's invertible), then its determinant, computed with the `LinearMap.det` function, is also a unit. This highlights an important property of determinants in linear algebra: the determinant of an endomorphism is a unit if and only if the endomorphism itself is a unit.
More concisely: If `f : M -> M` is a linear map over a commutative ring `A` with `f` being a unit, then `LinearMap.det f` is also a unit.
|
Basis.det_ne_zero
theorem Basis.det_ne_zero :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
[inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Basis ι R M) [inst_5 : Nontrivial R], e.det ≠ 0
The theorem `Basis.det_ne_zero` asserts that for any commutative ring `R`, any additive commutative group `M` that is also a module over `R`, any type `ι` with decidable equality and finite number of elements, and any basis `e` of `M` indexed by `ι`, the determinant of the basis `e` is not equal to zero, given that `R` is nontrivial. This effectively means that the determinant of a basis of a module is always nonzero when the underlying ring is nontrivial.
More concisely: For any commutative ring R that is nontrivial, any additive commutative group M that is an R-module with a finite basis e indexed by a type ι with decidable equality, the determinant of e is nonzero.
|
LinearMap.det_id
theorem LinearMap.det_id :
∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M],
LinearMap.det LinearMap.id = 1
This theorem states that for any module `M` over a commutative ring `A`, the determinant of the identity linear map on `M` is `1`. The identity linear map is defined as the map that leaves every element of `M` unchanged. The determinant of a linear map is a generalization of the determinant of a matrix, and in this case, it's similar to how the determinant of the identity matrix is `1`.
More concisely: For any commutative ring `A` and module `M` over `A`, the determinant of the identity linear map on `M` equals 1.
|
LinearMap.finiteDimensional_of_det_ne_one
theorem LinearMap.finiteDimensional_of_det_ne_one :
∀ {M : Type u_2} [inst : AddCommGroup M] {𝕜 : Type u_7} [inst_1 : Field 𝕜] [inst_2 : Module 𝕜 M] (f : M →ₗ[𝕜] M),
LinearMap.det f ≠ 1 → FiniteDimensional 𝕜 M
The theorem `LinearMap.finiteDimensional_of_det_ne_one` states that for any type `M` that forms an additive commutative group, and any type `𝕜` that forms a field with `M` being a module over `𝕜`, if a linear map `f` from `M` to `M` has a determinant that is not equal to `1`, then the vector space `M` over the field `𝕜` is finite-dimensional. In other words, if the determinant of a linear map differs from `1`, then the space the map operates on must have a finite basis.
More concisely: If `M` is a finite-dimensional additive commutative group over the field `𝕜` and the determinant of a linear map `f` from `M` to `M` is not equal to 1, then `M` is a finite-dimensional vector space over `𝕜`.
|
LinearEquiv.isUnit_det'
theorem LinearEquiv.isUnit_det' :
∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] (f : M ≃ₗ[A] M),
IsUnit (LinearMap.det ↑f)
This theorem, `LinearEquiv.isUnit_det'`, states that for any linear equivalence `f` from a type `M` to itself, where `M` is an additive commutative group and `A` is a commutative ring, and `M` is an `A`-module, the determinant of the linear map corresponding to `f` is a unit. In other words, the determinant of any linear equivalence in this context has a multiplicative inverse, meaning that it is non-zero when considered within the given commutative ring `A`.
More concisely: Given a linear equivalence `f` from an additive commutative group `M` to itself, which is an `A`-module over a commutative ring `A`, the determinant of the corresponding linear map is a unit in `A`.
|
LinearEquiv.det_conj
theorem LinearEquiv.det_conj :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_3}
[inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M ≃ₗ[R] M) (e : M ≃ₗ[R] M'),
LinearEquiv.det (e.symm ≪≫ₗ f ≪≫ₗ e) = LinearEquiv.det f
This theorem states that for any commutative ring `R` and for any `R`-modules `M` and `M'`, if `f` is a linear equivalence between `M` and itself and `e` is a linear equivalence between `M` and `M'`, then the determinant of the linear equivalence resulting from conjugating `f` by `e` (i.e., the composition of the inverse of `e`, `f`, and `e` in that order) is equal to the determinant of `f`. In more mathematical terms, we have $\det(e^{-1} \circ f \circ e) = \det(f)$, meaning that the determinant is invariant under conjugation by a linear equivalence.
More concisely: The determinant of a linear equivalence between modules, when conjugated by another linear equivalence, is equal to the determinant of the original linear equivalence.
|
Basis.det_self
theorem Basis.det_self :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
[inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Basis ι R M), e.det ⇑e = 1
The theorem `Basis.det_self` states that for any commutative ring `R`, any additive commutative group `M` that is also a module over the ring `R`, and any finite type `ι` with decidable equality, if `e` is a basis of `M` with respect to `R` and `ι`, then the determinant of the basis `e` evaluated at the basis `e` is 1. In other words, the determinant of the matrix representation of a basis with respect to itself is always 1.
More concisely: For any commutative ring R, additive commutative group M as an R-module with finite decidable equality basis e, the determinant of e evaluated at e equals 1.
|
Matrix.det_conj_of_mul_eq_one
theorem Matrix.det_conj_of_mul_eq_one :
∀ {A : Type u_5} [inst : CommRing A] {m : Type u_6} {n : Type u_7} [inst_1 : Fintype m] [inst_2 : Fintype n]
[inst_3 : DecidableEq m] [inst_4 : DecidableEq n] {M : Matrix m n A} {M' : Matrix n m A} {N : Matrix n n A},
M * M' = 1 → M' * M = 1 → (M * N * M').det = N.det
This theorem, `Matrix.det_conj_of_mul_eq_one`, states that if you have a commutative ring `A`, types `m` and `n` that are finite types and that have decidable equality, and matrices `M`, `M'`, and `N` with entries in `A` such that `M` and `M'` are two-sided inverses of each other (that is, `M * M'` and `M' * M` both equal the identity matrix), then the determinant of the matrix product `M * N * M'` is equal to the determinant of `N`.
This theorem generalizes the property of determinants where the determinant of a product of matrices is equal to the product of their determinants when the matrices are mutual inverses. It might be used in situations where you want to show that a certain transformation doesn't change the determinant of a matrix.
More concisely: If matrices `M`, `M'`, and `N` over a commutative ring `A` with decidable equality have dimensions `m x m`, `m' x m'`, and `m x n` respectively, and `M * M'` and `M' * M` are the identity matrices, then the determinant of `M * N * M'` equals the determinant of `N`.
|
Mathlib.LinearAlgebra.Determinant._auxLemma.3
theorem Mathlib.LinearAlgebra.Determinant._auxLemma.3 :
∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M]
(f g : M →ₗ[A] M), LinearMap.det f * LinearMap.det g = LinearMap.det (f ∘ₗ g)
This theorem states that, for any two endomorphisms `f` and `g` of a module `M` over a commutative ring `A` (i.e., linear transformations from `M` to itself), the determinant of the composition of `f` and `g` is equal to the product of the determinant of `f` and the determinant of `g`. This is a statement of the multiplicative property of determinants in linear algebra. If `M` does not have a finite basis, then the determinant is defined to be `1`, and the theorem holds trivially.
More concisely: For any two endomorphisms of a module over a commutative ring, the determinant of their composition equals the product of their determinants. If the module does not have a finite basis, then both determinants are equal to 1.
|
LinearMap.det_smul
theorem LinearMap.det_smul :
∀ {𝕜 : Type u_7} [inst : Field 𝕜] {M : Type u_8} [inst_1 : AddCommGroup M] [inst_2 : Module 𝕜 M] (c : 𝕜)
(f : M →ₗ[𝕜] M), LinearMap.det (c • f) = c ^ FiniteDimensional.finrank 𝕜 M * LinearMap.det f
This theorem states that for a given scalar `c` and a linear map `f` from a module `M` over a field `𝕜`, the determinant of the map `f` scaled by `c`, is equal to `c` raised to the power of the rank of `M` (interpreted as the finite dimension of `M` over `𝕜` when `M` is a vector space) times the determinant of the original map `f`. In mathematical terms, it essentially says that det(c*f) = c^(dim M) * det(f), where 'det' denotes determinant, 'dim' is the dimension of the module (or the rank of the vector space), and '*' denotes multiplication.
More concisely: The determinant of a linear map `f` from a module `M` of finite dimension over a field `𝕜`, scaled by a scalar `c`, equals `c` raised to the power of the module's dimension, multiplied by the determinant of `f`. In other words, det(`c*f`) = `c^(dim M) * det(f)`.
|
LinearMap.bot_lt_ker_of_det_eq_zero
theorem LinearMap.bot_lt_ker_of_det_eq_zero :
∀ {M : Type u_2} [inst : AddCommGroup M] {𝕜 : Type u_7} [inst_1 : Field 𝕜] [inst_2 : Module 𝕜 M] {f : M →ₗ[𝕜] M},
LinearMap.det f = 0 → ⊥ < LinearMap.ker f
This theorem states that if the determinant of a linear map `f` is zero, then the kernel of `f` is nontrivial. In other words, there exists at least one non-zero element in the domain `M` that `f` maps to the zero element of `M`. Here, `M` is a module over a field `𝕜`, and `f` is a linear map from `M` to itself. This is a way to express the fact that a linear map (or matrix) with a zero determinant cannot be injective (one-to-one).
More concisely: If the determinant of a linear map `f` from a module `M` over a field to itself is zero, then `f` has a non-zero kernel element in `M`.
|
AlternatingMap.eq_smul_basis_det
theorem AlternatingMap.eq_smul_basis_det :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
[inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Basis ι R M) (f : M [⋀^ι]→ₗ[R] R), f = f ⇑e • e.det
This theorem states that for any alternating map `f` to a commutative ring `R` where the indexing set `ι` has the same cardinality as a basis of a module `M` over `R`, `f` is equivalent to the determinant of that basis `e` multiplied by the value of `f` evaluated at `e`. This means that any alternating map can be expressed in terms of the determinant map with respect to a basis, scaled by the value of the alternating map on that basis.
More concisely: For any alternating map `f` from an indexing set `ι` of the same cardinality as a basis `e` of a commutative ring `R`-module `M`, `f` is equivalent to the determinant of `e` multiplied by `f` applied to `e`.
|
Basis.det_unitsSMul_self
theorem Basis.det_unitsSMul_self :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
[inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Basis ι R M) (w : ι → Rˣ),
e.det ⇑(e.unitsSMul w) = Finset.univ.prod fun i => ↑(w i)
The theorem `Basis.det_unitsSMul_self` states that for any commutative ring `R`, any additive commutative group `M`, any R-module structure on `M`, any type `ι` with decidable equality and finiteness, a basis `e` of the R-module `M` indexed by `ι`, and a function `w` mapping each index to a unit in `R`, the determinant of the basis obtained by scaling `e` by the units `w` is equal to the product of the units `w(i)` for all `i` in the universal finite set of `ι`.
More concisely: For any commutative ring R, additive commutative group M with an R-module structure, indexed type ι with decidable equality and finiteness, basis e of M indexed by ι, and function w mapping each index to a unit in R, the determinant of the basis obtained by scaling e with units w equals the product of the units w(i) for all i in ι.
|
Basis.det_unitsSMul
theorem Basis.det_unitsSMul :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
[inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Basis ι R M) (w : ι → Rˣ),
(e.unitsSMul w).det = ↑(Finset.univ.prod fun i => w i)⁻¹ • e.det
This theorem states that for a given basis `e` in a module `M` over a commutative ring `R`, if each column of the basis is scaled by certain units `w : ι → Rˣ` (where `ι` is the indexing set for the basis), the determinant of the basis changes in a specific way. Namely, the determinant of the new basis is the original determinant `e.det` scaled by the reciprocal of the product of all scalars `w i` (for all `i` in the index set `ι`). Here, `Finset.univ.prod fun i => w i` calculates the product of all the scalars `w i` as `i` ranges over the entire index set `ι`.
More concisely: Given a basis `e` in a module `M` over a commutative ring `R` and units `w : ι → Rˣ` for the indexing set `ι`, the determinant of the basis scaled by `w` is equal to the original determinant multiplied by the reciprocal of the product of all `w i`.
|
Basis.det_isUnitSMul
theorem Basis.det_isUnitSMul :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
[inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Basis ι R M) {w : ι → R} (hw : ∀ (i : ι), IsUnit (w i)),
e.det ⇑(e.isUnitSMul hw) = Finset.univ.prod fun i => w i
The theorem `Basis.det_isUnitSMul` states that, for any commutative ring `R`, an additive commutative group `M`, a module `M` over the ring `R`, and any basis `e` of `M` indexed by type `ι` (which has decidable equality and is finite), if we have a function `w` from `ι` to `R` such that each `w i` is a unit in the ring, then the determinant of the basis obtained by multiplying each basis vector by its corresponding unit `w i` (an operation denoted by `e.isUnitSMul hw`) is equal to the product of all the units `w i` (for `i` in the universal finite set of type `ι`).
More concisely: Given a commutative ring `R`, a finite, decidably-equaled indexed basis `e` of an `R`-module `M`, and a function `w : ι → R` with each `w i` being a unit, the determinant of `e.isUnitSMul hw` equals the product of all `w i`.
|
LinearMap.det_cases
theorem LinearMap.det_cases :
∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M]
[inst_3 : DecidableEq M] {P : A → Prop} (f : M →ₗ[A] M),
(∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((LinearMap.toMatrix b b) f).det) →
P 1 → P (LinearMap.det f)
The theorem `LinearMap.det_cases` states that for any additive commutative group `M`, any commutative ring `A`, any module `A M`, any endomorphism `f` of `M`, and any predicate `P` over `A`, if `P` holds for the determinant of the matrix representation of `f` with respect to any basis, and `P` holds for `1`, then `P` must hold for the determinant of `f`. This theorem allows us to prove properties about the determinant of a linear map by considering its matrix representation. Note that `A` is the scalar field, `M` is the vector space, and `M →ₗ[A] M` is a linear map from `M` to `M`. The determinant of a linear map or matrix is a concept from linear algebra that measures the "scaling factor" of the transformation represented by the map or matrix.
More concisely: If `M` is an additive commutative group, `A` is a commutative ring, `A → M` is an `A`-module, `f : M →ₗ[A] M` is an endomorphism, and for any basis of `M`, the determinant of `f`'s matrix representation satisfies a predicate `P` and `P` holds for 1, then the determinant of `f` also satisfies `P`.
|
LinearEquiv.det_mul_det_symm
theorem LinearEquiv.det_mul_det_symm :
∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] (f : M ≃ₗ[A] M),
LinearMap.det ↑f * LinearMap.det ↑f.symm = 1
This theorem states that for any linear equivalence `f` from a module `M` over a commutative ring `A` back to `M`, the product of the determinant of `f` and the determinant of its inverse equals 1. In other words, in the context of linear algebra, if `f` represents a change of basis in a finite-dimensional vector space over a field, then the determinant of this linear transformation multiplied by the determinant of its inverse (which represents the reverse change of basis) is always 1. This is analogous to the property of matrices where the determinant of a matrix multiplied by the determinant of its inverse is 1.
More concisely: For any linear endomorphism `f` of a finite-dimensional module `M` over a commutative ring `A`, the determinant of `f` multiplied by the determinant of its inverse equals the multiplicative identity element in `A`.
|
LinearEquiv.det_symm_mul_det
theorem LinearEquiv.det_symm_mul_det :
∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] (f : M ≃ₗ[A] M),
LinearMap.det ↑f.symm * LinearMap.det ↑f = 1
The theorem `LinearEquiv.det_symm_mul_det` states that for any linear equivalence `f` between a module `M` over a commutative ring `A` and itself, the determinant of the inverse of `f` multiplied by the determinant of `f` is equal to `1`. This theorem generalizes the property from linear algebra that the product of the determinant of a square matrix and the determinant of its inverse is `1`.
More concisely: For any linear equivalence `f` between a module `M` over a commutative ring `A`, `det(f) * det(f⁻¹) = 1`.
|
LinearMap.det_zero
theorem LinearMap.det_zero :
∀ {𝕜 : Type u_7} [inst : Field 𝕜] {M : Type u_8} [inst_1 : AddCommGroup M] [inst_2 : Module 𝕜 M],
LinearMap.det 0 = 0 ^ FiniteDimensional.finrank 𝕜 M
The theorem `LinearMap.det_zero` asserts that for any field `𝕜` and any module `M` over `𝕜`, the determinant of the zero map (which is a linear map sending every element of `M` to the zero element) is equal to zero raised to the power of the rank of the module `M`. This theorem holds for both finite-dimensional vector spaces and infinite-dimensional spaces. In the latter case, by convention, the determinant is defined to be `1`. In a finite-dimensional vector space, the determinant of the zero map is `1` if the dimension is `0` and `0` otherwise.
More concisely: For any field and module, the determinant of the zero linear map is equal to 0 raised to the power of the module's rank.
|
LinearMap.det_conj
theorem LinearMap.det_conj :
∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] {N : Type u_7}
[inst_3 : AddCommGroup N] [inst_4 : Module A N] (f : M →ₗ[A] M) (e : M ≃ₗ[A] N),
LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f
This theorem states that conjugating a linear map by a linear equivalence does not change its determinant. In other words, for any linear map `f` from a type `M` to itself, and a linear equivalence `e` between `M` and another type `N`, both over a commutative ring `A`, the determinant of the linear map resulting from conjugating `f` by `e` (i.e., applying `e`, then `f`, then the inverse of `e`) is the same as the determinant of `f` itself. This is a property that holds generally for linear maps and their determinants, and it is part of linear algebra theory.
More concisely: The determinant of a linear map conjugated by a linear equivalence is equal to the determinant of the original linear map.
|
Basis.det_apply
theorem Basis.det_apply :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
[inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Basis ι R M) (v : ι → M), e.det v = (e.toMatrix v).det
The theorem `Basis.det_apply` states that, for any commutative ring `R`, any type `M` forming an additive commutative group and an `R`-module, any finite type `ι`, any basis `e` of type `M` over `R` indexed by `ι`, and any family of vectors `v` (indexed by `ι` and of type `M`), the determinant of the vectors `v` with respect to the basis `e` is equal to the determinant of the matrix representation of the vectors `v` in the basis `e`. In other words, it asserts that the determinant computed directly from the vectors and the determinant computed from their matrix representation in a certain basis are the same.
More concisely: For any commutative ring R, any additive commutative group and R-module M, finite index type ι, basis e of M over R, and family v of vectors in M indexed by ι, the determinant of the vectors v with respect to the basis e equals the determinant of the matrix representation of the vectors v in the basis e.
|
LinearMap.det_toMatrix
theorem LinearMap.det_toMatrix :
∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
[inst_3 : CommRing A] [inst_4 : Module A M] (b : Basis ι A M) (f : M →ₗ[A] M),
((LinearMap.toMatrix b b) f).det = LinearMap.det f
The theorem `LinearMap.det_toMatrix` states that for any type `M` with an additive commutative group structure, type `ι` with decidable equality and is a finite type, type `A` with a commutative ring structure, and `A` is a module over `M`, given a basis `b` of `ι` over `A` for `M` and a linear map `f` from `M` to `M`, the determinant of the matrix representation of the linear map `f` with respect to the basis `b` is equal to the determinant of the linear map `f` itself. This establishes a correspondence between the determinant of a linear map and the determinant of its matrix representation in a given basis.
More concisely: For any linear map `f` between additive commutative groups `M` with decidable equality and finite indexing type `ι`, having a commutative ring structure and being a module over `M`, with respect to a basis `b` of `ι` over `A` for `M`, the determinant of the matrix representation of `f` with respect to `b` equals the determinant of `f` itself.
|
LinearMap.range_lt_top_of_det_eq_zero
theorem LinearMap.range_lt_top_of_det_eq_zero :
∀ {M : Type u_2} [inst : AddCommGroup M] {𝕜 : Type u_7} [inst_1 : Field 𝕜] [inst_2 : Module 𝕜 M] {f : M →ₗ[𝕜] M},
LinearMap.det f = 0 → LinearMap.range f < ⊤
The theorem `LinearMap.range_lt_top_of_det_eq_zero` states that, for any endomorphism `f` of a 𝕜-module `M`, if the determinant of `f` is zero, then the range of `f` is not the whole of `M`. In other words, `f` is not a surjective (or onto) function if its determinant equals zero. Here, `M` is a module over a field `𝕜`, which means that `M` is an additive commutative group equipped with a scalar multiplication by elements of `𝕜`.
More concisely: If the determinant of an endomorphism of a module over a field is zero, then the range of the endomorphism is strictly contained in the module.
|
Matrix.det_comm'
theorem Matrix.det_comm' :
∀ {A : Type u_5} [inst : CommRing A] {m : Type u_6} {n : Type u_7} [inst_1 : Fintype m] [inst_2 : Fintype n]
[inst_3 : DecidableEq m] [inst_4 : DecidableEq n] {M : Matrix n m A} {N M' : Matrix m n A},
M * M' = 1 → M' * M = 1 → (M * N).det = (N * M).det
This theorem states that for any types `A`, `m`, and `n`, where `A` is a commutative ring, `m` and `n` are finite types with decidable equality, and `M`, `N`, and `M'` are matrices with entries in `A`, rows indexed by `n` (`m` for `N` and `M'`) and columns indexed by `m` (`n` for `N` and `M'`), if `M` and `M'` are two-sided inverses (meaning that `M * M'` and `M' * M` both equal the identity matrix), then the determinant of `M * N` equals the determinant of `N * M`. This is a statement about the commutativity of determinant in the presence of a two-sided inverse.
More concisely: If matrices `M` and `M'` of compatible sizes over a commutative ring `A` with decidable equality and finite dimensions are two-sided inverses, then the determinant of `M * N` equals the determinant of `N * M` for any matrix `N` of compatible size with `M` and `M'`.
|
LinearMap.detAux_def'
theorem LinearMap.detAux_def' :
∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
[inst_3 : CommRing A] [inst_4 : Module A M] (b : Basis ι A M) (f : M →ₗ[A] M),
(LinearMap.detAux (Trunc.mk b)) f = ((LinearMap.toMatrix b b) f).det
This theorem, `LinearMap.detAux_def'`, states that for any additive commutative group `M`, type `ι` with decidable equality and finite type, a commutative ring `A`, and a module `M` over `A`, given a basis `b` of `M` over `A` and a linear map `f` from `M` to `M`, the determinant of the auxiliary linear map `detAux` applied to the truncated basis `b` and the linear map `f` is equal to the determinant of the matrix representation of the linear map `f` with respect to the basis `b`. The determinant of a matrix gives a scalar value which provides key insights into the matrix, such as whether it's invertible, and in this context, reveals properties about the linear map `f`.
More concisely: Given a commutative ring `A`, a finite type `ι`, an additive commutative group `M` with decidable equality, a basis `b` of `M` over `A`, and a linear map `f` from `M` to `M`, the determinant of the auxiliary linear map `detAux` applied to `b` and `f` is equal to the determinant of the matrix representation of `f` with respect to `b`.
|