Some obvious lemmas on module.End #
This file contains some obvious lemmas on module.End.
theorem
linear_map.comp_one
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[semiring R]
[add_comm_monoid E]
[add_comm_monoid F]
[module R F]
[module R E]
(f : E →ₗ[R] F) :
theorem
linear_map.one_comp
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[semiring R]
[add_comm_monoid E]
[add_comm_monoid F]
[module R F]
[module R E]
(f : E →ₗ[R] F) :
theorem
linear_map.comp_sum
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(g : M₃ →ₗ[R] M₂)
{α : Type u_5}
(s : finset α)
(f : α → (M →ₗ[R] M₃)) :
theorem
linear_map.sum_comp
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →ₗ[R] M₃)
{α : Type u_5}
(s : finset α)
(g : α → (M₃ →ₗ[R] M₂)) :
theorem
module.End.has_eigenvector_iff_has_eigenvalue
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{T : module.End R M}
{α : R} :