Some obvious lemmas on module.End #
This file contains some obvious lemmas on module.End.
theorem
LinearMap.comp_one
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[Semiring R]
[AddCommMonoid E]
[AddCommMonoid F]
[Module R F]
[Module R E]
(f : E →ₗ[R] F)
:
f ∘ₗ 1 = f
theorem
LinearMap.one_comp
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[Semiring R]
[AddCommMonoid E]
[AddCommMonoid F]
[Module R F]
[Module R E]
(f : E →ₗ[R] F)
:
1 ∘ₗ f = f
theorem
LinearMap.comp_sum
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
(g : M₃ →ₗ[R] M₂)
{α : Type u_5}
(s : Finset α)
(f : α → M →ₗ[R] M₃)
:
g ∘ₗ ∑ a ∈ s, f a = ∑ a ∈ s, g ∘ₗ f a
theorem
LinearMap.sum_comp
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
(f : M →ₗ[R] M₃)
{α : Type u_5}
(s : Finset α)
(g : α → M₃ →ₗ[R] M₂)
:
(∑ a ∈ s, g a) ∘ₗ f = ∑ a ∈ s, g a ∘ₗ f
theorem
Module.End.has_eigenvector_iff_hasEigenvalue
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
{T : Module.End R M}
{α : R}
: