Fundamentals

InstanceProduct of vector spaces#

Mathlib states this as Prod.instModule.

Prod.instModule.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R]
  [AddCommMonoid M] [AddCommMonoid N] [_root_.Module R M] [_root_.Module R N] :
  _root_.Module R (M × N)
Sources
MathlibProd.instModule
Uses 1 · Used by 16
Statement usesModule
Used byJensen's inequality (finite sum version) · Implicit function theorem · Leibniz formula (Analysis) · Orthogonal projection · Fundamental theorem of calculus, part 1 · Regularization by convolution · Smooth immersion · (smooth) direct sum of vector bundles · Structure theorem · Jacobson density theorem · Lie's theorem · Fernique's theorem · Closed graph theorem · Whitney embedding theorem · Change of variables to polar co-ordinates · Cauchy formulas

AbbreviationVector subspace#

Subspace of a vector space. Defined to equal Submodule.

Subspace.{u, v} (R : Type u) (M : Type v) [DivisionRing R] [AddCommGroup M] [_root_.Module R M] :
  Type v
Sources
MathlibSubspace
Uses 3 · Used by 2
Statement usesModule · Rational number · Ring
Used byHahn-Banach theorem · Sylvester's law of inertia (uniqueness)

InstanceSum of subspaces#

Mathlib states this as Submodule.completeLattice.

Submodule.completeLattice.{u_1, u_3} {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M]
  [_root_.Module R M] : CompleteLattice (Submodule R M)
Sources
MathlibSubmodule.completeLattice
Uses 1 · Used by 21
Statement usesModule
Used byImplicit function theorem · Existence of Hilbert basis · Orthogonal projection · Nullstellensatz · Going-up and going-down theorems · Jacobson density theorem · Krull's principal ideal theorem · Lasker–Noether theorem · Wedderburn–Artin theorem · M. Riesz extension theorem · Hahn embedding theorem · Ax–Grothendieck theorem · Whitney embedding theorem · Ostrowski's theorem · Complementary subspaces · Schur's lemma (Linear representations) · Generalized eigenspaces · Invariant subspaces of an endomorphism · Jordan-Chevalley-Dunford decomposition · Change of variables to polar co-ordinates · Bézout's identity

DefinitionDirect sum#

The DirectSum formed by a collection of additive submonoids (or subgroups, or submodules) of M is said to be internal if the canonical map (⨁ i, A i) →+ M is bijective.

For the alternate statement in terms of independence and spanning, see DirectSum.subgroup_isInternal_iff_iSupIndep_and_supr_eq_top and DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top.

DirectSum.IsInternal.{v, u_1, u_2} {ι : Type v} {M : Type u_1} {S : Type u_2} [DecidableEq ι]
  [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ι → S) : Prop
Sources
MathlibDirectSum.IsInternal
Uses 2 · Used by 3
Statement usesFinite set · Natural number
Used byTensor algebra of a commutative ring · Diagonalization of self-adjoint endomorphisms · Structure theorem

TheoremComplementary subspaces#

Mathlib states this as Submodule.exists_isCompl.

Submodule.exists_isCompl.{u_3, u_4} {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V]
  [_root_.Module K V] (p : Submodule K V) : ∃ q, IsCompl p q
Sources
MathlibSubmodule.exists_isCompl
Uses 5 · Used by 2
Statement usesRational number · Ring · Sum of subspaces
Proof usesExistence of bases · Kernel of a linear map
Used byRademacher's theorem · Maschke theorem

DefinitionLinear independence#

LinearIndependent R v states the family of vectors v is linearly independent over R.

LinearIndependent.{u', u_2, u_4} {ι : Type u'} (R : Type u_2) {M : Type u_4} (v : ι → M)
  [Semiring R] [AddCommMonoid M] [_root_.Module R M] : Prop
Sources
MathlibLinearIndependent
Uses 2 · Used by 26
Statement usesFinitely supported function · Linear map
Used byMinkowski’s Fundamental Theorem · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Sphere · Diagonalization of self-adjoint endomorphisms · Structure theorem · Dimension theorem for vector spaces · Rank–nullity theorem · Lie's theorem · Schur's lemma (1000+ theorems) · Intersecting secants theorem · Helly's theorem · Whitney embedding theorem · Cocyclicity · Inscribed angle theorem · Orthonormal bases · Adjoint endomorphism · Complex classification · Sylvester's law of inertia (existence) · Sylvester's law of inertia (uniqueness) · General linear group (Classical automorphism groups) · Rank of a linear map · Rank of a set of vectors · Existence of bases · Schur's lemma (Linear representations) · Rank of a matrix · Continuity (continuity and differentiability of convex functions)

DefinitionGenerating sets#

The span of a set s ⊆ M is the smallest submodule of M that contains s.

Submodule.span.{u_1, u_2} (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M]
  [_root_.Module R M] (s : Set M) : Submodule R M
Sources
MathlibSubmodule.span
Uses 1 · Used by 21
Statement usesModule
Used byExistence of Hilbert basis · Principal ideal domain · Hilbert basis theorem · Noetherian ring · Affine span · Minimal tensor product · Jacobi/Leibniz identity · Finite-dimensionality · Noetherian module · Going-up and going-down theorems · Jacobson density theorem · Dimension theorem for vector spaces · Lie's theorem · M. Riesz extension theorem · Cocyclicity · Gram-Schmidt orthogonalisation · Rank of a set of vectors · Existence of bases · Weierstrass trigonometric approximation theorem · Taylor's theorem with Lagrange form for remainder · Example, the Hilbert basis of trigonometric polynomials

DefinitionExistence of bases#

Each vector space has a basis.

Module.Basis.ofVectorSpace.{u_3, u_4} (K : Type u_3) (V : Type u_4) [DivisionRing K]
  [AddCommGroup V] [_root_.Module K V] : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex K V)) K V
Sources
MathlibModule.Basis.ofVectorSpace
Uses 5 · Used by 2
Statement usesBasis · Generating sets · Linear independence · Range of a linear map · Rational number
Used byFinite-dimensional normed spaces over complete normed fields are complete · Complementary subspaces

DefinitionRange of a linear map#

The range of a linear map f : M → M₂ is a submodule of M₂. See Note [range copy pattern].

LinearMap.range.{u_1, u_2, u_5, u_6} {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6}
  [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [_root_.Module R M]
  [_root_.Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
  Submodule R₂ M₂
Sources
MathlibLinearMap.range
Uses 1 · Used by 22
Statement usesLinear map
Used byImplicit function theorem · Existence of Hilbert basis · Fréchet-Riesz representation of the dual of a Hilbert space · Orthogonal projection · Dual basis · Diagonalization of self-adjoint endomorphisms · Isomorphism with bidual · Structure theorem · Jacobson density theorem · Rank–nullity theorem · Wedderburn–Artin theorem · Lie's theorem · Closed graph theorem · Inscribed angle theorem · Orthonormal bases · Adjoint endomorphism · Sylvester's law of inertia (existence) · Rank of a linear map · Existence of bases · Rank of a matrix · Fourier transform on \(\mathrm{L}^2(\R^d)\) · Example, the Hilbert basis of trigonometric polynomials

DefinitionKernel of a linear map#

The kernel of a linear map f : M → M₂ is defined to be comap f ⊥. This is equivalent to the set of x : M such that f x = 0. The kernel is a submodule of M.

LinearMap.ker.{u_1, u_2, u_5, u_6} {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6}
  [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [_root_.Module R M]
  [_root_.Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) : Submodule R M
Sources
MathlibLinearMap.ker
Uses 1 · Used by 14
Statement usesLinear map
Used byImplicit function theorem · Lax-Milgram theorem · Finite-dimensional normed spaces over complete normed fields are complete · Structure theorem · Jacobson density theorem · Rank–nullity theorem · Whitney embedding theorem · Decomposition of an orthogonal transformation as a product of reflections · Maschke theorem · Orthogonality · Complementary subspaces · Generalized eigenspaces · Fourier transform on \(\mathrm{L}^2(\R^d)\) · Change of variables to polar co-ordinates

InstanceAlgebra of endomorphisms of a vector space#

Mathlib states this as Module.End.instAlgebra.

Module.End.instAlgebra.{u, v, w} (R : Type u) (S : Type v) (M : Type w) [CommSemiring R]
  [Semiring S] [AddCommMonoid M] [_root_.Module R M] [_root_.Module S M] [SMulCommClass S R M]
  [SMul R S] [IsScalarTower R S M] : Algebra R (Module.End S M)
Sources
MathlibModule.End.instAlgebra
Uses 2 · Used by 12
Statement usesAssociative algebra over a commutative ring · Linear map
Used byApproximation by convolution · Divergence theorem · Scheme · Cayley-Hamilton theorem · Existence of an eigenvalue · Mean of product of independent random variables · Wedderburn–Artin theorem · Lie's theorem · \(L^p\) functions · Multiplication by a function \(C^\infty\) of slow growth · Determinant of endomorphisms · Jordan-Chevalley-Dunford decomposition

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.