NormalBasis

📁 Source: Mathlib/FieldTheory/Galois/NormalBasis.lean

Statistics

Metric	Count
Definitions normalBasis	1
Theorems normalBasis_apply, exists_linearIndependent_algEquiv_apply	2
Total	3

IsGalois

Definitions

Name	Category	Theorems
normalBasis 📖	CompOp	1 math math: normalBasis_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normalBasis_apply 📖	mathematical	—	DFunLike.coe Module.Basis AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Module.Basis.instFunLike normalBasis AlgEquiv.instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid AlgEquiv.aut	—	exists_linearIndependent_algEquiv_apply coe_basisOfLinearIndependentOfCardEqFinrank AlgEquiv.one_apply

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_linearIndependent_algEquiv_apply 📖	mathematical	—	LinearIndependent AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring DFunLike.coe AlgEquiv.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule	—	finite_or_infinite Module.finite_of_finite

---

← Back to Index