Theorems · Definition · linear algebra

LinearMap.iterateKer

{R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (M →ₗ[R] M) → ℕ →o Submodule R M

The increasing sequence of submodules consisting of the kernels of the iterates of a linear map.

Defined in: Mathlib.Algebra.Module.Submodule.Ker
Cited by: 5 results in Mathlib
Foundations: Depth 28 from the axioms · uses propext, Quot.sound
Assumes: Semiring AddCommMonoid Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
RingHom.idstatement and proof · cited by 18,349
Semiringstatement and proof · cited by 13,802
AddCommMonoidstatement and proof · cited by 12,281
LinearMapstatement and proof · cited by 10,215
Submodulestatement · cited by 7,192
OrderHomstatement · cited by 934
LinearMap.kerproof · cited by 848

Cited by5

Results whose statement or proof uses this declaration.

Module.End.mem_genEigenspaceproof · cited by 4
Module.End.mem_genEigenspace_natproof · cited by 4
LinearMap.eventually_iSup_ker_pow_eqproof · cited by 2
Module.End.eventually_disjoint_ker_pow_range_powproof · cited by 1
LinearMap.iterateKer_coestatement and proof · cited by 1