FLT/Mathlib/Topology/Algebra/Module/FiniteDimension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite Dimension

Material destined for Mathlib.

Imports (4)
Imported by 2 files
  1. theorem Basis.toMatrix_continuous line 21 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: AddCommGroup, Finite, TopologicalSpace, NontriviallyNormedField, Module, IsTopologicalAddGroup, ContinuousSMul, CompleteSpace, T2Space, FiniteDimensional, Module.Basis, Continuous, Matrix, Module.Basis.toMatrix

    Proof uses: Fintype, Fintype.ofFinite, LinearMap.continuous_of_finiteDimensional, RingHom.id, Module.Basis.toMatrixEquiv

    92 instances, coercions and auxiliary constants left out.