Documentation

Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Finite and free modules using matrices #

We provide some instances for finite and free modules involving matrices.

Main results #

instance Module.Free.linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module S N] [SMulCommClass R S N] [Module.Free S N] :
Equations
  • =
instance Module.Finite.linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module S N] [SMulCommClass R S N] [Module.Finite S N] :
Equations
  • =

The finrank of M →ₗ[R] N as an S-module is (finrank R M) * (finrank S N).

@[deprecated Module.finrank_linearMap_self]

Alias of Module.finrank_linearMap_self.

instance Finite.algHom (K : Type u_1) (M : Type u_2) (L : Type v) [CommRing K] [Ring M] [Algebra K M] [Module.Free K M] [Module.Finite K M] [CommRing L] [IsDomain L] [Algebra K L] :
Equations
  • =
theorem card_algHom_le_finrank (K : Type u_1) (M : Type u_2) (L : Type v) [CommRing K] [Ring M] [Algebra K M] [Module.Free K M] [Module.Finite K M] [CommRing L] [IsDomain L] [Algebra K L] :
theorem Matrix.rank_vecMulVec {K : Type u} {m : Type u} {n : Type u} [CommRing K] [Fintype n] [DecidableEq n] (w : mK) (v : nK) :
(Matrix.toLin' (Matrix.vecMulVec w v)).rank 1