FiniteDimensional

📁 Source: Mathlib/LinearAlgebra/Matrix/FiniteDimensional.lean

Statistics

Metric	Count
Definitions	0
Theorems finiteDimensional, finiteDimensional', finiteDimensional	3
Total	3

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteDimensional 📖	mathematical	—	FiniteDimensional LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Field.toDivisionRing addCommGroup module DivisionRing.toDivisionSemiring smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing	—	Module.Finite.linearMap Module.Free.of_divisionRing smulCommClass_self
finiteDimensional' 📖	mathematical	—	FiniteDimensional LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Field.toDivisionRing addCommGroup module DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring IsScalarTower.to_smulCommClass' Semifield.toCommSemiring Field.toSemifield	—	FiniteDimensional.of_injective IsScalarTower.to_smulCommClass' smulCommClass_self IsScalarTower.compatibleSMul restrictScalars_injective finiteDimensional

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteDimensional 📖	mathematical	—	FiniteDimensional Matrix Field.toDivisionRing addCommGroup Ring.toAddCommGroup DivisionRing.toRing module DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring Semiring.toModule	—	Module.Finite.matrix Module.Free.self FiniteDimensional.finiteDimensional_self

---

← Back to Index