PowerBasis

📁 Source: Mathlib/RingTheory/PowerBasis.lean

Statistics

Metric	Count
Definitions PowerBasis, PowerBasis, fintype, basis, dim, equivOfMinpoly, equivOfRoot, gen, liftEquiv, liftEquiv', map, minpolyGen	12
Theorems mem_span_pow, PowerBasis_gen, adjoin_eq_top_of_gen_mem_adjoin, adjoin_gen_eq_top, aeval_minpolyGen, algHom_ext, basis_eq_pow, coe_basis, constr_pow_aeval, constr_pow_algebraMap, constr_pow_gen, constr_pow_mul, degree_minpoly, degree_minpolyGen, dim_le_degree_of_root, dim_le_natDegree_of_root, dim_ne_zero, dim_pos, equivOfMinpoly_aeval, equivOfMinpoly_apply, equivOfMinpoly_gen, equivOfMinpoly_map, equivOfMinpoly_symm, equivOfRoot_aeval, equivOfRoot_apply, equivOfRoot_gen, equivOfRoot_map, equivOfRoot_symm, exists_eq_aeval, exists_eq_aeval', exists_gen_dvd_sub, exists_smodEq, finite, finrank, isIntegral_gen, leftMulMatrix, liftEquiv'_apply_coe, liftEquiv'_symm_apply_apply, liftEquiv_apply_coe, liftEquiv_symm_apply, lift_aeval, lift_gen, map_basis, map_dim, map_gen, mem_span_pow, mem_span_pow', minpolyGen_eq, minpolyGen_map, minpolyGen_monic, natDegree_minpoly, natDegree_minpolyGen, linearIndependent_pow	53
Total	65

IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_span_pow 📖	mathematical	IsIntegral DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule SetLike.instMembership Submodule.setLike Submodule.span Set.range Polynomial.natDegree minpoly Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	PowerBasis.mem_span_pow' minpoly.monic LT.lt.trans_le Polynomial.degree_modByMonic_lt Polynomial.degree_le_natDegree Polynomial.modByMonic_add_div Polynomial.aeval_add map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass minpoly.aeval MulZeroClass.zero_mul add_zero

Module.Basis

Definitions

Name	Category	Theorems
PowerBasis 📖	CompOp	1 math math: PowerBasis_gen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
PowerBasis_gen 📖	mathematical	DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring instFunLike Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Fintype.card Equiv EquivLike.toFunLike Equiv.instEquivLike	PowerBasis.gen PowerBasis	—	—

PowerBasis

Definitions

Name	Category	Theorems
basis 📖	CompOp	31 math math: IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow, IsCyclotomicExtension.discr_odd_prime, map_basis, IsCyclotomicExtension.Rat.discr_prime_pow', Algebra.discr_powerBasis_eq_norm, leftMulMatrix, coe_basis, charpoly_leftMulMatrix, constr_pow_algebraMap, IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, repr_gen_pow_isIntegral, Algebra.embeddingsMatrixReindex_eq_vandermonde, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', IsCyclotomicExtension.discr_prime_pow_ne_two, IsAdjoinRootMonic.powerBasis_basis, constr_pow_gen, toMatrix_isIntegral, basis_eq_pow, Algebra.discr_mul_isIntegral_mem_adjoin, Algebra.discr_powerBasis_eq_prod, Algebra.discr_powerBasis_eq_prod'', Algebra.discr_powerBasis_eq_prod', liftEquiv'_symm_apply_apply, constr_pow_mul, Module.Basis.traceDual_powerBasis_eq, IsCyclotomicExtension.Rat.discr_odd_prime', constr_pow_aeval, Algebra.traceForm_toMatrix_powerBasis, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', IsCyclotomicExtension.discr_prime_pow, IsCyclotomicExtension.discr_prime_pow_ne_two'
dim 📖	CompOp	57 math math: exists_eq_aeval, IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow, Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly, IsCyclotomicExtension.discr_odd_prime, ofAdjoinEqTop'_dim, map_dim, IsAdjoinRootMonic.powerBasis_dim, map_basis, IsPrimitiveRoot.powerBasis_dim, AdjoinRoot.powerBasis'_dim, IsCyclotomicExtension.Rat.discr_prime_pow', finrank, Algebra.discr_powerBasis_eq_norm, leftMulMatrix, coe_basis, natDegree_minpolyGen, charpoly_leftMulMatrix, constr_pow_algebraMap, Algebra.adjoin.powerBasis_dim, IsPrimitiveRoot.power_basis_int'_dim, IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, repr_gen_pow_isIntegral, Algebra.embeddingsMatrixReindex_eq_vandermonde, IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim, degree_minpoly, Algebra.adjoin.powerBasis'_dim, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', IsCyclotomicExtension.discr_prime_pow_ne_two, constr_pow_gen, AlgHom.card_of_powerBasis, toMatrix_isIntegral, basis_eq_pow, Algebra.discr_mul_isIntegral_mem_adjoin, IsPrimitiveRoot.subOnePowerBasis_dim, dim_pos, Algebra.discr_powerBasis_eq_prod, ofGenMemAdjoin'_dim, AdjoinRoot.powerBasis_dim, degree_minpolyGen, AlgHom.natCard_of_powerBasis, IsPrimitiveRoot.integralPowerBasis_dim, ofAdjoinEqTop_dim, Algebra.discr_powerBasis_eq_prod'', dim_le_natDegree_of_root, Algebra.discr_powerBasis_eq_prod', liftEquiv'_symm_apply_apply, constr_pow_mul, Module.Basis.traceDual_powerBasis_eq, IsCyclotomicExtension.Rat.discr_odd_prime', natDegree_minpoly, constr_pow_aeval, Algebra.traceForm_toMatrix_powerBasis, dim_le_degree_of_root, IntermediateField.adjoin.powerBasis_dim, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', IsCyclotomicExtension.discr_prime_pow, IsCyclotomicExtension.discr_prime_pow_ne_two'
equivOfMinpoly 📖	CompOp	6 math math: equivOfMinpoly_map, equivOfMinpoly_gen, equivOfMinpoly_aeval, equivOfMinpoly_apply, equivOfMinpoly_symm, IsCyclotomicExtension.autEquivPow_symm_apply
equivOfRoot 📖	CompOp	5 math math: equivOfRoot_symm, equivOfRoot_apply, equivOfRoot_aeval, equivOfRoot_map, equivOfRoot_gen
gen 📖	CompOp	65 math math: IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime, exists_eq_aeval, Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly, isIntegral_gen, quotientEquivQuotientMinpolyMap_apply, IsPrimitiveRoot.subOneIntegralPowerBasis_gen, equivAdjoinSimple_symm_aeval, AdjoinRoot.powerBasis'_gen, IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_one, Algebra.discr_powerBasis_eq_norm, quotientEquivQuotientMinpolyMap_apply_mk, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime, map_gen, IntermediateField.adjoin.powerBasis_gen, leftMulMatrix, quotientEquivQuotientMinpolyMap_symm_apply_mk, coe_basis, IsPrimitiveRoot.powerBasis_gen, charpoly_leftMulMatrix, IsPrimitiveRoot.integralPowerBasis'_gen, liftEquiv_symm_apply, equivAdjoinSimple_aeval, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen, trace_gen_eq_nextCoeff_minpoly, exists_smodEq, IsAdjoinRootMonic.powerBasis_gen, adjoin_gen_eq_top, Algebra.embeddingsMatrixReindex_eq_vandermonde, sum_embeddings_eq_finrank_mul, degree_minpoly, equivAdjoinSimple_gen, equivAdjoinSimple_symm_gen, Algebra.adjoin.powerBasis_gen, basis_eq_pow, quotientEquivQuotientMinpolyMap_symm_apply, IsPrimitiveRoot.subOnePowerBasis_gen, ofAdjoinEqTop_gen, Algebra.discr_powerBasis_eq_prod, exists_eq_aeval', minpolyGen_eq, exists_gen_dvd_sub, Module.Basis.PowerBasis_gen, liftEquiv'_apply_coe, Algebra.adjoin.powerBasis'_minpoly_gen, AdjoinRoot.minpoly_powerBasis_gen, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, Algebra.discr_powerBasis_eq_prod'', IsPrimitiveRoot.integralPowerBasis_gen, Algebra.discr_powerBasis_eq_prod', liftEquiv'_symm_apply_apply, conductor_eq_top_of_powerBasis, Module.Basis.traceDual_powerBasis_eq, Algebra.adjoin.powerBasis'_gen, ofAdjoinEqTop'_gen, natDegree_minpoly, aeval_minpolyGen, Algebra.traceForm_toMatrix_powerBasis, AdjoinRoot.minpoly_powerBasis_gen_of_monic, Algebra.prod_embeddings_eq_finrank_pow, ofGenMemAdjoin'_gen, WeierstrassCurve.Affine.CoordinateRing.basis_apply, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen_prime, AdjoinRoot.powerBasis_gen, liftEquiv_apply_coe
liftEquiv 📖	CompOp	2 math math: liftEquiv_symm_apply, liftEquiv_apply_coe
liftEquiv' 📖	CompOp	2 math math: liftEquiv'_apply_coe, liftEquiv'_symm_apply_apply
map 📖	CompOp	4 math math: map_dim, map_basis, map_gen, minpolyGen_map
minpolyGen 📖	CompOp	7 math math: minpolyGen_monic, leftMulMatrix, natDegree_minpolyGen, minpolyGen_map, minpolyGen_eq, degree_minpolyGen, aeval_minpolyGen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_eq_top_of_gen_mem_adjoin 📖	mathematical	Subalgebra CommRing.toCommSemiring Ring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet gen	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	eq_top_iff adjoin_gen_eq_top Algebra.adjoin_le
adjoin_gen_eq_top 📖	mathematical	—	Algebra.adjoin CommRing.toCommSemiring Ring.toSemiring Set Set.instSingletonSet gen Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Algebra.toSubmodule_eq_top eq_top_iff Module.Basis.span_eq Submodule.span_le basis_eq_pow Subalgebra.pow_mem Algebra.subset_adjoin Set.mem_singleton
aeval_minpolyGen 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval gen minpolyGen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_sum Finset.sum_congr map_mul NonUnitalAlgSemiHomClass.toMulHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Polynomial.aeval_C Polynomial.aeval_X sub_eq_zero RingHomInvPair.ids Module.Basis.linearCombination_repr Finsupp.linearCombination_apply Finsupp.sum_fintype coe_basis zero_smul
algHom_ext 📖	—	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike gen	—	—	AlgHom.ext exists_eq_aeval' Polynomial.aeval_algHom_apply AlgHom.algHomClass
basis_eq_pow 📖	mathematical	—	DFunLike.coe Module.Basis dim CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring Module.Basis.instFunLike basis Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero gen	—	—
coe_basis 📖	mathematical	—	DFunLike.coe Module.Basis dim CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring Module.Basis.instFunLike basis Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero gen	—	basis_eq_pow
constr_pow_aeval 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Pi.addCommMonoid dim LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.constr basis Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	subsingleton_or_nontrivial RingHomInvPair.ids smulCommClass_self Unique.instSubsingleton Polynomial.aeval_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Polynomial.aeval_modByMonic_eq_self_of_root minpoly.monic isIntegral_gen minpoly.aeval MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass natDegree_minpoly Polynomial.natDegree_lt_natDegree Polynomial.degree_modByMonic_lt Polynomial.aeval_eq_sum_range' map_sum Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass Finset.mem_range basis_eq_pow Module.Basis.constr_basis
constr_pow_algebraMap 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Pi.addCommMonoid dim LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.constr basis Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom RingHom.instFunLike algebraMap	—	RingHomInvPair.ids smulCommClass_self Polynomial.aeval_C constr_pow_aeval
constr_pow_gen 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Pi.addCommMonoid dim LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.constr basis Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	RingHomInvPair.ids smulCommClass_self Polynomial.aeval_X constr_pow_aeval
constr_pow_mul 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Pi.addCommMonoid dim LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.constr basis Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	RingHomInvPair.ids smulCommClass_self exists_eq_aeval' constr_pow_aeval
degree_minpoly 📖	mathematical	—	Polynomial.degree CommSemiring.toSemiring CommRing.toCommSemiring minpoly gen WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne dim	—	minpolyGen_eq degree_minpolyGen
degree_minpolyGen 📖	mathematical	—	Polynomial.degree CommSemiring.toSemiring CommRing.toCommSemiring minpolyGen WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne dim	—	Polynomial.degree_sub_eq_left_of_degree_lt Polynomial.degree_X_pow Polynomial.degree_sum_fin_lt
dim_le_degree_of_root 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne dim Polynomial.degree	—	Polynomial.degree_eq_natDegree WithBot.coe_le_coe dim_le_natDegree_of_root
dim_le_natDegree_of_root 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	dim Polynomial.natDegree	—	le_of_not_gt Polynomial.as_sum_range' Finset.sum_range Fintype.sum_eq_zero Fintype.linearIndependent_iff Module.Basis.linearIndependent Finset.sum_congr basis_eq_pow Polynomial.aeval_eq_sum_range' Polynomial.monomial_zero_right
dim_ne_zero 📖	—	—	—	—	not_nonempty_iff Fin.isEmpty Module.Basis.index_nonempty
dim_pos 📖	mathematical	—	dim	—	dim_ne_zero
equivOfMinpoly_aeval 📖	mathematical	minpoly gen	DFunLike.coe AlgEquiv CommRing.toCommSemiring Ring.toSemiring AlgEquiv.instFunLike equivOfMinpoly AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	equivOfRoot_aeval
equivOfMinpoly_apply 📖	mathematical	minpoly gen	DFunLike.coe AlgEquiv CommRing.toCommSemiring Ring.toSemiring AlgEquiv.instFunLike equivOfMinpoly AlgHom AlgHom.funLike lift	—	—
equivOfMinpoly_gen 📖	mathematical	minpoly gen	DFunLike.coe AlgEquiv CommRing.toCommSemiring Ring.toSemiring AlgEquiv.instFunLike equivOfMinpoly	—	equivOfRoot_gen
equivOfMinpoly_map 📖	mathematical	minpoly gen CommRing.toRing map	equivOfMinpoly	—	equivOfRoot_map
equivOfMinpoly_symm 📖	mathematical	minpoly gen	AlgEquiv.symm CommRing.toCommSemiring Ring.toSemiring equivOfMinpoly Polynomial CommSemiring.toSemiring	—	—
equivOfRoot_aeval 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval gen minpoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	AlgEquiv AlgEquiv.instFunLike equivOfRoot	—	lift_aeval
equivOfRoot_apply 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval gen minpoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	AlgEquiv AlgEquiv.instFunLike equivOfRoot lift	—	—
equivOfRoot_gen 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval gen minpoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	AlgEquiv AlgEquiv.instFunLike equivOfRoot	—	lift_gen
equivOfRoot_map 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval gen minpoly CommRing.toRing map MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	equivOfRoot	—	AlgEquiv.ext exists_eq_aeval' AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass equivOfRoot_aeval Polynomial.aeval_algEquiv
equivOfRoot_symm 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval gen minpoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	AlgEquiv.symm equivOfRoot	—	—
exists_eq_aeval 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring dim DFunLike.coe AlgHom Polynomial Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval gen	—	mem_span_pow dim_ne_zero coe_basis Module.Basis.mem_span
exists_eq_aeval' 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval gen	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim exists_eq_aeval
exists_gen_dvd_sub 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing gen CommRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	Ideal.instIsTwoSided_1 map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass exists_smodEq
exists_smodEq 📖	mathematical	—	SModEq CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal.span Set Set.instSingletonSet gen DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	subsingleton_or_nontrivial SModEq.eq_1 Subsingleton.eq_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHomInvPair.ids dim_pos Module.Basis.sum_repr add_zero Submodule.Quotient.mk_add Finset.sum_insert Finset.notMem_erase Finset.insert_erase Finset.mem_univ Ideal.instIsTwoSided_1 coe_basis pow_zero Algebra.algebraMap_eq_smul_one Submodule.Quotient.mk_zero Submodule.Quotient.mk_eq_zero Ideal.sum_mem Algebra.smul_def' Ideal.mul_mem_left Ideal.pow_mem_of_mem Ideal.subset_span
finite 📖	mathematical	—	Module.Finite CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring	—	Module.Finite.of_basis Finite.of_fintype
finrank 📖	mathematical	—	Module.finrank CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring dim	—	Module.finrank_eq_card_basis Fintype.card_fin
isIntegral_gen 📖	mathematical	—	IsIntegral gen	—	minpolyGen_monic aeval_minpolyGen
leftMulMatrix 📖	mathematical	—	DFunLike.coe AlgHom Matrix dim CommRing.toCommSemiring Ring.toSemiring Matrix.semiring CommSemiring.toSemiring Fin.fintype Matrix.instAlgebra Algebra.id AlgHom.funLike Algebra.leftMulMatrix basis gen Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Polynomial.coeff minpolyGen AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	subsingleton_or_nontrivial Matrix.subsingleton RingHomInvPair.ids smulCommClass_self Finite.of_fintype IsScalarTower.left Algebra.leftMulMatrix_apply LinearEquiv.eq_symm_apply LinearMap.toMatrix_symm Module.Basis.ext Matrix.toLin_self Finset.sum_congr basis_eq_pow pow_succ' neg_smul Finset.sum_neg_distrib add_comm Polynomial.aeval_eq_sum_range Finset.sum_range_succ Polynomial.leadingCoeff.eq_1 Polynomial.Monic.leadingCoeff minpolyGen_monic one_smul natDegree_minpolyGen Finset.sum_range aeval_minpolyGen lt_of_le_of_ne Fintype.sum_eq_single zero_smul
liftEquiv'_apply_coe 📖	mathematical	—	Multiset Multiset.instMembership Polynomial.aroots minpoly gen DFunLike.coe Equiv AlgHom CommRing.toCommSemiring Ring.toSemiring CommSemiring.toSemiring EquivLike.toFunLike Equiv.instEquivLike liftEquiv' CommRing.toRing AlgHom.funLike	—	—
liftEquiv'_symm_apply_apply 📖	mathematical	—	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring CommRing.toRing AlgHom.funLike Equiv Multiset Multiset.instMembership Polynomial.aroots minpoly gen CommSemiring.toSemiring EquivLike.toFunLike Equiv.instEquivLike Equiv.symm liftEquiv' LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike LinearEquiv Pi.addCommMonoid dim LinearMap.addCommMonoid Pi.Function.module LinearMap.module DFinsupp.instEquivLikeLinearEquiv Module.Basis.constr basis Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
liftEquiv_apply_coe 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Equiv EquivLike.toFunLike Equiv.instEquivLike liftEquiv	—	—
liftEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing EquivLike.toFunLike Equiv.instEquivLike Equiv.symm liftEquiv lift	—	—
lift_aeval 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	lift	—	constr_pow_aeval
lift_gen 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	lift	—	constr_pow_gen
map_basis 📖	mathematical	—	basis CommRing.toRing map Module.Basis.map dim CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring AlgEquiv.toLinearEquiv	—	—
map_dim 📖	mathematical	—	dim CommRing.toRing map	—	—
map_gen 📖	mathematical	—	gen CommRing.toRing map DFunLike.coe AlgEquiv CommRing.toCommSemiring Ring.toSemiring CommSemiring.toSemiring AlgEquiv.instFunLike	—	—
mem_span_pow 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike Submodule.span Set.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.natDegree DFunLike.coe AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	mem_span_pow' lt_of_le_of_ne Polynomial.degree_eq_natDegree WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero WithBot.bot_lt_coe
mem_span_pow' 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike Submodule.span Set.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne DFunLike.coe AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	Set.ext Finset.sum_congr Algebra.smul_def Polynomial.eval₂_eq_sum
minpolyGen_eq 📖	mathematical	—	minpolyGen minpoly gen	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton minpoly.unique' minpolyGen_monic aeval_minpolyGen LE.le.not_gt dim_le_degree_of_root degree_minpolyGen
minpolyGen_map 📖	mathematical	—	minpolyGen CommRing.toRing map	—	minpolyGen_eq minpoly.algEquiv_eq
minpolyGen_monic 📖	mathematical	—	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring minpolyGen	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Polynomial.Monic.sub_of_left Polynomial.monic_X_pow Polynomial.degree_X_pow Polynomial.degree_sum_fin_lt
natDegree_minpoly 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring minpoly gen dim	—	minpolyGen_eq natDegree_minpolyGen
natDegree_minpolyGen 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring minpolyGen dim	—	Polynomial.natDegree_eq_of_degree_eq_some degree_minpolyGen

PowerBasis.AlgHom

Definitions

Name	Category	Theorems
fintype 📖	CompOp	5 math math: sum_embeddings_eq_finrank_mul, AlgHom.card_of_powerBasis, trace_eq_sum_embeddings_gen, Algebra.norm_eq_prod_embeddings_gen, Algebra.prod_embeddings_eq_finrank_pow

(root)

Definitions

Name	Category	Theorems
PowerBasis 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearIndependent_pow 📖	mathematical	—	LinearIndependent Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain minpoly Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring	—	Fintype.linearIndependent_iff Function.mtr LE.le.not_gt minpoly.degree_le_of_ne_zero Finset.mem_univ Finset.sum_ite_eq' Finset.sum_congr Polynomial.coeff_monomial map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Algebra.smul_def Polynomial.degree_sum_fin_lt Polynomial.degree_eq_natDegree minpoly.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing minpoly.eq_zero Polynomial.natDegree_zero linearIndependent_empty_type Fin.isEmpty'

---

← Back to Index