Def LinearMap.iterateKer

Modification history

2024-02-14 03:21

Mathlib/Algebra/Module/Submodule/Ker.lean

chore: Move LinearMap.ker to a new file (#10233) …

Modified LinearMap.iterateKer View on Github →

2023-09-01 20:13

Mathlib/LinearAlgebra/Basic.lean

chore: tidy various files (#6838)

Modified LinearMap.iterateKer View on Github →

2023-02-13 06:07

Mathlib/LinearAlgebra/Basic.lean

feat: port LinearAlgebra.Basic (#1979)

Added LinearMap.iterateKer View on Github →