mathlib3 documentation

linear_algebra.free_module.finite.matrix

Finite and free modules using matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

source
@[protected, instance]
def module.free.linear_map (R : Type u) (M : Type v) (N : Type w) [comm_ring R] [add_comm_group M] [module R M] [module.free R M] [add_comm_group N] [module R N] [module.free R N] [module.finite R M] [module.finite R N] :
module.free R (M →ₗ[R] N)
source
@[protected, instance]
def module.finite.linear_map {R : Type u} (M : Type v) (N : Type w) [comm_ring R] [add_comm_group M] [module R M] [module.free R M] [add_comm_group N] [module R N] [module.free R N] [module.finite R M] [module.finite R N] :
module.finite R (M →ₗ[R] N)
source
@[protected, instance]
def module.finite.add_monoid_hom (M : Type v) (N : Type w) [add_comm_group M] [module.finite ℤ M] [module.free ℤ M] [add_comm_group N] [module.finite ℤ N] [module.free ℤ N] :
module.finite ℤ (M →+ N)
source
@[protected, instance]
def module.free.add_monoid_hom (M : Type v) (N : Type w) [add_comm_group M] [module.finite ℤ M] [module.free ℤ M] [add_comm_group N] [module.finite ℤ N] [module.free ℤ N] :
module.free ℤ (M →+ N)
source
theorem finite_dimensional.finrank_linear_map (R : Type u) (M : Type v) (N : Type w) [comm_ring R] [strong_rank_condition R] [add_comm_group M] [module R M] [module.free R M] [module.finite R M] [add_comm_group N] [module R N] [module.free R N] [module.finite R N] :
finite_dimensional.finrank R (M →ₗ[R] N) = finite_dimensional.finrank R M * finite_dimensional.finrank R N

The finrank of M →ₗ[R] N is (finrank R M) * (finrank R N).

source
theorem matrix.rank_vec_mul_vec {K m n : Type u} [comm_ring K] [strong_rank_condition K] [fintype n] [decidable_eq n] (w : m → K) (v : n → K) :
(⇑matrix.to_lin' (matrix.vec_mul_vec w v)).rank ≤ 1