/- Focused imports for the journal audit. No mathematical declarations. -/
import Mathlib.Algebra.Module.SpanRankOperations
import Mathlib.LinearAlgebra.FreeAlgebra
import Mathlib.LinearAlgebra.TensorProduct.Tower
import Mathlib.LinearAlgebra.TensorProduct.Prod
import Mathlib.LinearAlgebra.Matrix.ToLin
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.FiniteDimensional
import Mathlib.LinearAlgebra.Dimension.Constructions
import Mathlib.LinearAlgebra.Basis.VectorSpace
import Mathlib.LinearAlgebra.Eigenspace.Minpoly
import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
import Mathlib.RingTheory.AdjoinRoot
import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Analysis.InnerProductSpace.l2Space
import Mathlib.Analysis.InnerProductSpace.Adjoint
import Mathlib.Analysis.Normed.Module.Completion
import Mathlib.RingTheory.RootsOfUnity.Complex
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Module
import Mathlib.Tactic.Nontriviality
import Mathlib.Tactic.Push
import Mathlib.Tactic.Abel
import Mathlib.Tactic.FunProp
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Convert
import Mathlib.Tactic.Finiteness
import Mathlib.Tactic.IntervalCases
import Mathlib.Tactic.Ext
import Mathlib.Tactic.Tauto
import Mathlib.Util.AssertNoSorry
import Mathlib.Algebra.Order.Floor.Div
import Mathlib.LinearAlgebra.Charpoly.Basic
import Mathlib.LinearAlgebra.Lagrange
import Mathlib.RingTheory.Noetherian.Filter
import Mathlib.Algebra.Algebra.TransferInstance
import Mathlib.LinearAlgebra.Matrix.Module