Here are the libraries or modules needed: import algebra.big_operators.pi import algebra.module.hom import algebra.module.prod import algebra.module.submodule.lattice import data.dfinsupp.basic import data.finsupp.basic https://github.com/leanprover-community/mathlib/tree/master/src/linear_algebra - Basic theorems - https://github.com/leanprover-community/mathlib/blob/master/src/linear_algebra/basic.lean - Authors: [[Johannes Hölzl]], [[Mario Carneiro]], [[Kevin Buzzard]], [[Yury Kudryashov]], Frédéric Dupuis, [[Heather Macbeth]]