PowerBasis

📁 Source: Mathlib/RingTheory/Adjoin/PowerBasis.lean

Statistics

Metric	Count
Definitions ofGenMemAdjoin, powerBasis, powerBasisAux, ofAdjoinEqTop	4
Theorems powerBasis_dim, powerBasis_gen, ofAdjoinEqTop_dim, ofAdjoinEqTop_gen, repr_gen_pow_isIntegral, repr_mul_isIntegral, repr_pow_isIntegral, toMatrix_isIntegral	8
Total	12

Algebra.PowerBasis

Definitions

Name	Category	Theorems
ofGenMemAdjoin 📖	CompOp	—

Algebra.adjoin

Definitions

Name	Category	Theorems
powerBasis 📖	CompOp	2 math math: powerBasis_dim, powerBasis_gen
powerBasisAux 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
powerBasis_dim 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing	PowerBasis.dim Subalgebra Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet Subalgebra.toRing Subalgebra.algebra powerBasis Polynomial.natDegree minpoly	—	—
powerBasis_gen 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing	PowerBasis.gen Subalgebra Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet Subalgebra.toRing Subalgebra.algebra powerBasis	—	—

PowerBasis

Definitions

Name	Category	Theorems
ofAdjoinEqTop 📖	CompOp	2 math math: ofAdjoinEqTop_gen, ofAdjoinEqTop_dim

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofAdjoinEqTop_dim 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing Algebra.adjoin Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	dim ofAdjoinEqTop Polynomial.natDegree minpoly	—	—
ofAdjoinEqTop_gen 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing Algebra.adjoin Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	gen ofAdjoinEqTop	—	—
repr_gen_pow_isIntegral 📖	mathematical	IsIntegral CommRing.toRing gen minpoly Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring algebraMap	DFunLike.coe Finsupp dim MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid Algebra.toModule Ring.toSemiring Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basis Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim RingHomInvPair.ids Module.IsNoetherian.finite isNoetherian_of_finite Finite.of_subsingleton Polynomial.aeval_X_pow Polynomial.modByMonic_add_div minpoly.monic map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass minpoly.aeval MulZeroClass.zero_mul add_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass natDegree_minpoly Polynomial.Monic.natDegree_map Polynomial.natDegree_lt_natDegree_iff Polynomial.degree_modByMonic_lt Polynomial.Nontrivial.of_polynomial_ne Polynomial.aeval_eq_sum_range' map_sum Finset.sum_apply' IsIntegral.sum Finset.mem_range basis_eq_pow Algebra.smul_def IsScalarTower.algebraMap_apply map_smul SemilinearMapClass.toMulActionSemiHomClass algebraMap_smul Finsupp.isScalarTower IsScalarTower.right Module.Basis.repr_self_apply mul_one isIntegral_algebraMap smul_zero
repr_mul_isIntegral 📖	mathematical	IsIntegral CommRing.toRing gen DFunLike.coe Finsupp dim MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid Algebra.toModule Ring.toSemiring Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basis minpoly Polynomial.map algebraMap	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHomInvPair.ids Module.Basis.sum_repr Finset.sum_mul_sum Finset.sum_product' map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finset.sum_apply' IsIntegral.sum Algebra.mul_smul_comm Algebra.smul_mul_assoc MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass IsIntegral.mul coe_basis repr_gen_pow_isIntegral
repr_pow_isIntegral 📖	mathematical	IsIntegral CommRing.toRing gen DFunLike.coe Finsupp dim MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid Algebra.toModule Ring.toSemiring Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basis minpoly Polynomial.map algebraMap	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	RingHomInvPair.ids Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Nat.case_strong_induction_on pow_zero dim_pos basis_eq_pow Module.Basis.repr_self_apply isIntegral_one isIntegral_zero pow_succ repr_mul_isIntegral le_rfl
toMatrix_isIntegral 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval gen EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing IsIntegral minpoly Polynomial.map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield algebraMap	DivisionRing.toRing Field.toDivisionRing Module.Basis.toMatrix dim Semifield.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring basis Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids Module.Basis.toMatrix_apply coe_basis repr_pow_isIntegral Polynomial.aeval_eq_sum_range map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finset.sum_apply' IsIntegral.sum Algebra.smul_def IsScalarTower.algebraMap_apply map_smul SemilinearMapClass.toMulActionSemiHomClass algebraMap_smul Finsupp.isScalarTower IsScalarTower.right IsIntegral.smul IsScalarTower.left repr_gen_pow_isIntegral

---

← Back to Index