MathlibImports.lean

1 /- Focused imports for the journal audit. No mathematical declarations. -/
2 import Mathlib.Algebra.Module.SpanRankOperations
3 import Mathlib.LinearAlgebra.FreeAlgebra
4 import Mathlib.LinearAlgebra.TensorProduct.Tower
5 import Mathlib.LinearAlgebra.TensorProduct.Prod
6 import Mathlib.LinearAlgebra.Matrix.ToLin
7 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
8 import Mathlib.LinearAlgebra.Matrix.FiniteDimensional
9 import Mathlib.LinearAlgebra.Dimension.Constructions
10 import Mathlib.LinearAlgebra.Basis.VectorSpace
11 import Mathlib.LinearAlgebra.Eigenspace.Minpoly
12 import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
13 import Mathlib.RingTheory.AdjoinRoot
14 import Mathlib.Algebra.QuadraticAlgebra.Basic
15 import Mathlib.Analysis.InnerProductSpace.l2Space
16 import Mathlib.Analysis.InnerProductSpace.Adjoint
17 import Mathlib.Analysis.Normed.Module.Completion
18 import Mathlib.RingTheory.RootsOfUnity.Complex
19 import Mathlib.Tactic.Ring
20 import Mathlib.Tactic.Linarith
21 import Mathlib.Tactic.NormNum
22 import Mathlib.Tactic.FinCases
23 import Mathlib.Tactic.FieldSimp
24 import Mathlib.Tactic.Module
25 import Mathlib.Tactic.Nontriviality
26 import Mathlib.Tactic.Push
27 import Mathlib.Tactic.Abel
28 import Mathlib.Tactic.FunProp
29 import Mathlib.Tactic.Positivity
30 import Mathlib.Tactic.Convert
31 import Mathlib.Tactic.Finiteness
32 import Mathlib.Tactic.IntervalCases
33 import Mathlib.Tactic.Ext
34 import Mathlib.Tactic.Tauto
35 import Mathlib.Util.AssertNoSorry
36 import Mathlib.Algebra.Order.Floor.Div
37 import Mathlib.LinearAlgebra.Charpoly.Basic
38 import Mathlib.LinearAlgebra.Lagrange
39 import Mathlib.RingTheory.Noetherian.Filter
40 import Mathlib.Algebra.Algebra.TransferInstance
41 import Mathlib.LinearAlgebra.Matrix.Module

Back to source controls