Basic

📁 Source: Mathlib/RingTheory/Trace/Basic.lean

Statistics

Metric	Count
Definitions embeddingsMatrix, embeddingsMatrixReindex, traceMatrix, traceDual	4
Theorems embeddingsMatrixReindex_eq_vandermonde, embeddingsMatrix_apply, isIntegral_trace, isNilpotent_trace_of_isNilpotent, traceForm_toMatrix_powerBasis, traceMatrix_apply, traceMatrix_eq_embeddingsMatrixReindex_mul_trans, traceMatrix_eq_embeddingsMatrix_mul_trans, traceMatrix_of_basis, traceMatrix_of_basis_mulVec, traceMatrix_of_matrix_mulVec, traceMatrix_of_matrix_vecMul, traceMatrix_reindex, trace_eq_of_algEquiv, trace_eq_of_equiv_equiv, trace_eq_of_ringEquiv, trace_eq_zero_of_not_isSeparable, trace_isNilpotent_of_isNilpotent, trace_ne_zero, trace_surjective, trace_gen_eq_sum_roots, trace_gen_eq_zero, traceDual_def, traceDual_eq_iff, traceDual_inj, traceDual_injective, traceDual_involutive, traceDual_powerBasis_eq, traceDual_repr_apply, traceDual_traceDual, trace_mul_traceDual, trace_traceDual_mul, trace_gen_eq_nextCoeff_minpoly, trace_gen_eq_sum_roots, det_traceForm_ne_zero, det_traceMatrix_ne_zero', sum_embeddings_eq_finrank_mul, traceForm_nondegenerate, traceForm_nondegenerate_tfae, trace_adjoinSimpleGen, trace_eq_finrank_mul_minpoly_nextCoeff, trace_eq_sum_automorphisms, trace_eq_sum_embeddings, trace_eq_sum_embeddings_gen, trace_eq_sum_roots, trace_eq_trace_adjoin	46
Total	50

Algebra

Definitions

Name	Category	Theorems
embeddingsMatrix 📖	CompOp	2 math math: traceMatrix_eq_embeddingsMatrix_mul_trans, embeddingsMatrix_apply
embeddingsMatrixReindex 📖	CompOp	4 math math: NumberField.basisMatrix_eq_embeddingsMatrixReindex, embeddingsMatrixReindex_eq_vandermonde, discr_eq_det_embeddingsMatrixReindex_pow_two, traceMatrix_eq_embeddingsMatrixReindex_mul_trans
traceMatrix 📖	CompOp	10 math math: traceMatrix_apply, traceMatrix_localizationLocalization, traceMatrix_of_matrix_vecMul, traceMatrix_reindex, traceMatrix_eq_embeddingsMatrix_mul_trans, traceMatrix_of_basis, discr_def, traceMatrix_of_matrix_mulVec, traceMatrix_of_basis_mulVec, traceMatrix_eq_embeddingsMatrixReindex_mul_trans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
embeddingsMatrixReindex_eq_vandermonde 📖	mathematical	—	embeddingsMatrixReindex PowerBasis.dim CommRing.toRing DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toModule Ring.toSemiring Module.Basis.instFunLike PowerBasis.basis Matrix.transpose Matrix.vandermonde AlgHom AlgHom.funLike Equiv EquivLike.toFunLike Equiv.instEquivLike PowerBasis.gen	—	Matrix.ext PowerBasis.coe_basis map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
embeddingsMatrix_apply 📖	mathematical	—	embeddingsMatrix DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	—
isIntegral_trace 📖	mathematical	IsIntegral DivisionRing.toRing Field.toDivisionRing	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instFunLike trace	—	IsIntegral.tower_top isIntegral_algebraMap_iff AlgebraicClosure.instIsScalarTower RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing instIsDomain trace_eq_sum_roots IsAlgClosed.splits AlgebraicClosure.isAlgClosed IsIntegral.nsmul IsIntegral.multiset_sum minpoly.monic Polynomial.aeval_def minpoly.aeval_of_isScalarTower Polynomial.mem_roots_map minpoly.ne_zero
isNilpotent_trace_of_isNilpotent 📖	mathematical	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toModule Semiring.toModule LinearMap.instFunLike trace	—	LinearMap.isNilpotent_trace_of_isNilpotent IsNilpotent.map smulCommClass_self IsScalarTower.left RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
traceForm_toMatrix_powerBasis 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CommRing.toRing toModule Ring.toSemiring Matrix PowerBasis.dim LinearMap.addCommMonoid LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid to_smulCommClass id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix Fin.fintype PowerBasis.basis traceForm Equiv Equiv.instEquivLike Matrix.of NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LinearMap.instFunLike trace Monoid.toNatPow PowerBasis.gen	—	Matrix.ext RingHomInvPair.ids to_smulCommClass LinearMap.instSMulCommClass traceForm_toMatrix Matrix.of_apply pow_add PowerBasis.basis_eq_pow
traceMatrix_apply 📖	mathematical	—	traceMatrix DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonAssocSemiring.toNonUnitalNonAssocSemiring toModule Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module traceForm	—	—
traceMatrix_eq_embeddingsMatrixReindex_mul_trans 📖	mathematical	—	Matrix.map traceMatrix Field.toCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid embeddingsMatrixReindex Matrix.transpose	—	instIsDomain traceMatrix_eq_embeddingsMatrix_mul_trans embeddingsMatrixReindex.eq_1 Matrix.reindex_apply Matrix.transpose_submatrix Matrix.submatrix_mul_transpose_submatrix Equiv.coe_refl Equiv.refl_symm
traceMatrix_eq_embeddingsMatrix_mul_trans 📖	mathematical	—	Matrix.map traceMatrix Field.toCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Matrix AlgHom CommRing.toCommSemiring Matrix.instHMulOfFintypeOfMulOfAddCommMonoid minpoly.AlgHom.fintype DivisionRing.toRing Field.toDivisionRing instIsDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid embeddingsMatrix Matrix.transpose	—	Matrix.ext instIsDomain trace_eq_sum_embeddings Finset.sum_congr map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass
traceMatrix_of_basis 📖	mathematical	—	traceMatrix DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Module.Basis.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm Matrix LinearMap.addCommMonoid LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Matrix.addCommMonoid to_smulCommClass id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix traceForm	—	Matrix.ext RingHomInvPair.ids to_smulCommClass LinearMap.instSMulCommClass traceMatrix_apply traceForm_apply traceForm_toMatrix
traceMatrix_of_basis_mulVec 📖	mathematical	—	Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing traceMatrix DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toModule Module.Basis.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.equivFun Finite.of_fintype LinearMap LinearMap.instFunLike trace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	RingHomInvPair.ids Finite.of_fintype Matrix.replicateCol_apply Matrix.replicateCol_mulVec Matrix.mul_apply traceMatrix.eq_1 Finset.sum_congr mul_comm smul_eq_mul Matrix.of_apply map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass mul_smul_comm to_smulCommClass Finset.mul_sum Module.Basis.sum_equivFun
traceMatrix_of_matrix_mulVec 📖	mathematical	—	traceMatrix Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.transpose	—	AddEquiv.injective Matrix.transposeAddEquiv_apply Matrix.vecMul_transpose Matrix.transpose_map traceMatrix_of_matrix_vecMul Matrix.transpose_transpose
traceMatrix_of_matrix_vecMul 📖	mathematical	—	traceMatrix Matrix.vecMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.transpose	—	Matrix.ext traceMatrix_apply Matrix.vecMul.eq_1 dotProduct.eq_1 Matrix.mul_apply LinearMap.BilinForm.sum_left Fintype.sum_congr LinearMap.BilinForm.sum_right Finset.sum_comm Finset.sum_mul Matrix.map_apply traceForm_apply mul_comm smul_def smul_mul_assoc MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass mul_assoc mul_smul_comm map_smul
traceMatrix_reindex 📖	mathematical	—	traceMatrix DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Module.Basis.instFunLike Module.Basis.reindex Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex	—	Matrix.ext Module.Basis.coe_reindex
trace_eq_of_algEquiv 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instFunLike trace AlgEquiv AlgEquiv.instFunLike	—	smulCommClass_self IsScalarTower.left RingHomInvPair.ids LinearMap.trace_conj' LinearMap.ext map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.apply_symm_apply
trace_eq_of_equiv_equiv 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring algebraMap RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass	DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid toModule Semiring.toModule LinearMap.instFunLike trace RingEquiv.symm	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.map_mul' RingEquiv.map_add' trace_eq_of_ringEquiv trace_eq_of_algEquiv RingEquiv.symm_apply_apply
trace_eq_of_ringEquiv 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring algebraMap RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass	DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid toModule Semiring.toModule LinearMap.instFunLike trace	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass trace_eq_matrix_trace smul_def RingEquiv.apply_symm_apply AddMonoidHom.map_trace RingHomClass.toAddMonoidHomClass Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype to_smulCommClass IsScalarTower.right LinearEquiv.map_zero LinearMap.toMatrix_apply Module.Basis.coe_mapCoeffs trace_eq_zero_of_not_exists_basis LinearMap.zero_apply map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass
trace_eq_zero_of_not_isSeparable 📖	mathematical	IsSeparable Field.toCommRing DivisionRing.toRing Field.toDivisionRing	trace LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instZero	—	ExpChar.exists instIsDomain expChar_ne_zero LinearMap.ext CanLift.prf Subtype.canLift SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IntermediateField.algebraMap_apply IsScalarTower.left trace_trace IntermediateField.isScalarTower_mid' Module.Free.of_divisionRing IntermediateField.finiteDimensional_left IntermediateField.finiteDimensional_right trace_algebraMap commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing IsPurelyInseparable.finrank_eq_pow IntermediateField.expChar separableClosure.isPurelyInseparable IsAlgebraic.of_finite separableClosure.eq_top_iff IntermediateField.finrank_eq_one_iff_eq_top pow_zero one_pow pow_succ' SemigroupAction.mul_smul LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul AddCommMonoid.nat_isScalarTower IsScalarTower.right nsmul_eq_mul CharP.cast_eq_zero MulZeroClass.zero_mul LinearMap.zero_apply trace_eq_finrank_mul_minpoly_nextCoeff Irreducible.hasSeparableContraction minpoly.irreducible IsIntegral.isIntegral IsAlgebraic.isIntegral Polynomial.expand_one Polynomial.nextCoeff.eq_1 LT.lt.ne' minpoly.natDegree_pos Polynomial.coeff_expand pow_pos IsStrictOrderedRing.toPosMulStrictMono Nat.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Polynomial.natDegree_expand dvd_mul_left tsub_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le LT.lt.ne ne_of_gt mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono neg_zero MulZeroClass.mul_zero trace_eq_zero_of_not_exists_basis Module.Finite.of_basis Finite.of_fintype
trace_isNilpotent_of_isNilpotent 📖	mathematical	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toModule Semiring.toModule LinearMap.instFunLike trace	—	isNilpotent_trace_of_isNilpotent
trace_ne_zero 📖	—	—	—	—	List.TFAE.out traceForm_nondegenerate_tfae
trace_surjective 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instFunLike trace	—	RingHomSurjective.ids LinearMap.range_eq_top IsSimpleOrder.eq_bot_or_eq_top Ideal.isSimpleOrder LinearMap.range_eq_bot trace_ne_zero

IntermediateField.AdjoinSimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trace_gen_eq_sum_roots 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map CommSemiring.toSemiring Semifield.toCommSemiring algebraMap minpoly EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike LinearMap CommRing.toCommSemiring RingHom.id IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IntermediateField.toField Algebra.toModule IntermediateField.algebra' Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule LinearMap.instFunLike Algebra.trace gen Multiset.sum Polynomial.aroots instIsDomain	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing IsScalarTower.left instIsDomain IntermediateField.adjoin.powerBasis_gen PowerBasis.trace_gen_eq_sum_roots SubsemiringClass.nontrivial minpoly.algebraMap_eq IntermediateField.isScalarTower_mid' algebraMap_gen Polynomial.aroots.congr_simp trace_gen_eq_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass minpoly.eq_zero Polynomial.roots.congr_simp Polynomial.map_zero Polynomial.roots_zero
trace_gen_eq_zero 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IntermediateField.toField Algebra.toModule IntermediateField.algebra' Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule LinearMap.instFunLike Algebra.trace gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	IsScalarTower.left Algebra.trace_eq_zero_of_not_exists_basis Mathlib.Tactic.Contrapose.contrapose₄ IsIntegral.of_mem_of_fg Submodule.fg_iff_finiteDimensional Module.Basis.finiteDimensional_of_finite Finite.of_fintype IntermediateField.subset_adjoin Set.mem_singleton LinearMap.zero_apply

Module.Basis

Definitions

Name	Category	Theorems
traceDual 📖	CompOp	11 math math: traceDual_def, trace_traceDual_mul, trace_mul_traceDual, traceDual_traceDual, traceDual_inj, traceDual_involutive, traceDual_repr_apply, Submodule.traceDual_span_of_basis, traceDual_powerBasis_eq, traceDual_injective, traceDual_eq_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
traceDual_def 📖	mathematical	—	traceDual LinearMap.BilinForm.dualBasis Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Algebra.toModule CommRing.toCommSemiring Field.toCommRing CommSemiring.toSemiring Algebra.traceForm traceForm_nondegenerate	—	—
traceDual_eq_iff 📖	mathematical	—	DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Semifield.toCommSemiring instFunLike traceDual LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module Algebra.traceForm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	LinearMap.BilinForm.dualBasis_eq_iff traceForm_nondegenerate
traceDual_inj 📖	mathematical	—	traceDual	—	traceDual_injective
traceDual_injective 📖	mathematical	—	Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Semifield.toCommSemiring traceDual	—	LinearMap.BilinForm.dualBasis_injective traceForm_nondegenerate Algebra.traceForm_isSymm
traceDual_involutive 📖	mathematical	—	Function.Involutive Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Semifield.toCommSemiring traceDual	—	LinearMap.BilinForm.dualBasis_involutive traceForm_nondegenerate Algebra.traceForm_isSymm
traceDual_powerBasis_eq 📖	mathematical	—	DFunLike.coe Module.Basis PowerBasis.dim Field.toCommRing DivisionRing.toRing Field.toDivisionRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semifield.toCommSemiring instFunLike traceDual Finite.of_fintype Fin.fintype PowerBasis.basis DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring minpolyDiv PowerBasis.gen AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative minpoly	—	Finite.of_fintype traceDual_eq_iff RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing instIsDomain AlgHomClass.toRingHomClass AlgHom.algHomClass sum_smul_minpolyDiv_eq_X_pow AlgebraicClosure.isAlgClosed PowerBasis.adjoin_gen_eq_top Fin.prop PowerBasis.finrank commRing_strongRankCondition PowerBasis.coe_basis MonoidWithZeroHom.map_ite_one_zero RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finset.sum_congr Polynomial.map_smul map_div₀ map_pow MonoidWithZeroHomClass.toMonoidHomClass Polynomial.finset_sum_coeff Polynomial.coeff_smul Polynomial.coeff_map Polynomial.coeff_X_pow trace_eq_sum_embeddings map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_inv_one Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero
traceDual_repr_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Finsupp.instAddCommMonoid Algebra.toModule Semifield.toCommSemiring Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv repr traceDual LinearMap CommSemiring.toSemiring CommRing.toCommSemiring LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module Algebra.traceForm Module.Basis instFunLike	—	LinearMap.BilinForm.dualBasis_repr_apply traceForm_nondegenerate
traceDual_traceDual 📖	mathematical	—	traceDual	—	LinearMap.BilinForm.dualBasis_dualBasis traceForm_nondegenerate Algebra.traceForm_isSymm
trace_mul_traceDual 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule LinearMap.instFunLike Algebra.trace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semifield.toCommSemiring instFunLike traceDual AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	LinearMap.BilinForm.apply_dualBasis_right traceForm_nondegenerate Algebra.traceForm_isSymm
trace_traceDual_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule LinearMap.instFunLike Algebra.trace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semifield.toCommSemiring instFunLike traceDual AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	LinearMap.BilinForm.apply_dualBasis_left traceForm_nondegenerate

PowerBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trace_gen_eq_nextCoeff_minpoly 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule LinearMap.instFunLike Algebra.trace gen CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Polynomial.nextCoeff minpoly	—	dim_pos natDegree_minpoly IsLocalRing.toNontrivial Field.instIsLocalRing Algebra.trace_eq_matrix_trace Matrix.trace_eq_neg_charpoly_coeff charpoly_leftMulMatrix Fintype.card_fin Polynomial.nextCoeff_of_natDegree_pos
trace_gen_eq_sum_roots 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map CommSemiring.toSemiring Semifield.toCommSemiring algebraMap minpoly EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing gen	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike LinearMap CommRing.toCommSemiring RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule LinearMap.instFunLike Algebra.trace Multiset.sum Polynomial.aroots instIsDomain	—	instIsDomain trace_gen_eq_nextCoeff_minpoly map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Polynomial.nextCoeff_map_eq DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic Polynomial.Monic.map minpoly.monic isIntegral_gen neg_neg

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_traceForm_ne_zero 📖	—	—	—	—	Module.Basis.finiteDimensional_of_finite Finite.of_fintype RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass LinearMap.BilinForm.toMatrix_mul_basis_toMatrix Matrix.det_comm' Module.Basis.toMatrix_mul_toMatrix_flip Matrix.mul_assoc Matrix.det_mul mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain IsUnit.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid Matrix.det.congr_simp Matrix.transpose_mul Matrix.transpose_one Matrix.mul_one Matrix.det_one Algebra.traceMatrix_of_basis det_traceMatrix_ne_zero'
det_traceMatrix_ne_zero' 📖	—	—	—	—	instIsDomain PowerBasis.finite AlgHom.card AlgebraicClosure.isAlgClosed PowerBasis.finrank commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing RingHom.map_det RingHom.mapMatrix_apply Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans Algebra.embeddingsMatrixReindex_eq_vandermonde Matrix.det_mul Matrix.det_transpose mul_self_eq_zero IsDomain.to_noZeroDivisors Matrix.det_vandermonde LT.lt.ne' Finset.mem_Ioi Equiv.injective PowerBasis.algHom_ext map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
sum_embeddings_eq_finrank_mul 📖	mathematical	—	Finset.sum AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Finset.univ minpoly.AlgHom.fintype DivisionRing.toRing Field.toDivisionRing instIsDomain DFunLike.coe AlgHom.funLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap PowerBasis.gen AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.finrank Algebra.toModule CommRing.toCommSemiring Ring.toSemiring PowerBasis.AlgHom.fintype	—	instIsDomain FiniteDimensional.right Fintype.sum_equiv Finset.univ_sigma_univ Finset.sum_sigma Finset.sum_nsmul Finset.sum_congr Finset.sum_const AlgHom.card Algebra.isSeparable_tower_top_of_isSeparable
traceForm_nondegenerate 📖	mathematical	—	LinearMap.BilinForm.Nondegenerate CommRing.toCommSemiring Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.traceForm	—	LinearMap.BilinForm.nondegenerate_of_det_ne_zero instIsDomain commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing det_traceForm_ne_zero
traceForm_nondegenerate_tfae 📖	mathematical	—	List.TFAE Algebra.IsSeparable Field.toCommRing DivisionRing.toRing Field.toDivisionRing LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule Algebra.trace LinearMap.instZero LinearMap.BilinForm.Nondegenerate Algebra.traceForm	—	traceForm_nondegenerate LinearMap.BilinForm.Nondegenerate.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing LinearMap.BilinForm.ext not_imp_comm Algebra.trace_eq_zero_of_not_isSeparable List.tfae_of_cycle
trace_adjoinSimpleGen 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IntermediateField.toField Algebra.toModule IntermediateField.algebra' Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule LinearMap.instFunLike Algebra.trace IntermediateField.AdjoinSimple.gen NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Polynomial.nextCoeff minpoly	—	IsScalarTower.left IntermediateField.minpoly_gen PowerBasis.trace_gen_eq_nextCoeff_minpoly SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsLocalRing.toNontrivial Field.instIsLocalRing
trace_eq_finrank_mul_minpoly_nextCoeff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule LinearMap.instFunLike Algebra.trace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Module.finrank IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IntermediateField.toField IntermediateField.instModuleSubtypeMem NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Polynomial.nextCoeff minpoly	—	IsScalarTower.left trace_eq_trace_adjoin trace_adjoinSimpleGen IsIntegral.of_finite Algebra.smul_def
trace_eq_sum_automorphisms 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap LinearMap CommRing.toCommSemiring Field.toCommRing RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule LinearMap.instFunLike Algebra.trace Finset.sum AlgEquiv Finset.univ AlgEquiv.fintype AlgEquiv.instFunLike	—	FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass instIsDomain Fintype.sum_equiv AlgebraicClosure.instIsScalarTower IsScalarTower.right IsGalois.to_normal AlgHom.restrictNormal_commutes trace_eq_sum_embeddings AlgebraicClosure.isAlgClosed IsGalois.to_isSeparable Algebra.algebraMap_eq_smul_one smul_one_smul
trace_eq_sum_embeddings 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap LinearMap CommRing.toCommSemiring Field.toCommRing RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule LinearMap.instFunLike Algebra.trace Finset.sum AlgHom Finset.univ minpoly.AlgHom.fintype DivisionRing.toRing Field.toDivisionRing instIsDomain AlgHom.funLike	—	Algebra.IsSeparable.isIntegral IsScalarTower.left instIsDomain trace_eq_trace_adjoin Algebra.smul_def map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass IntermediateField.adjoin.powerBasis_gen trace_eq_sum_embeddings_gen IsAlgClosed.splits Algebra.IsSeparable.isSeparable Algebra.isSeparable_tower_bot_of_isSeparable IsLocalRing.toNontrivial Field.instIsLocalRing IntermediateField.isScalarTower_mid' algebraMap_smul AddCommMonoid.nat_isScalarTower sum_embeddings_eq_finrank_mul
trace_eq_sum_embeddings_gen 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map CommSemiring.toSemiring Semifield.toCommSemiring algebraMap minpoly Field.toCommRing DivisionRing.toRing Field.toDivisionRing PowerBasis.gen IsSeparable	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike LinearMap CommRing.toCommSemiring RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule LinearMap.instFunLike Algebra.trace Finset.sum AlgHom Ring.toSemiring Finset.univ PowerBasis.AlgHom.fintype instIsDomain AlgHom.funLike	—	instIsDomain PowerBasis.trace_gen_eq_sum_roots IsLocalRing.toNontrivial Field.instIsLocalRing Fintype.sum_equiv PowerBasis.liftEquiv'_apply_coe Finset.sum_mem_multiset Finset.sum_eq_multiset_sum Multiset.toFinset_val Multiset.dedup_eq_self Polynomial.nodup_roots Polynomial.separable_map Multiset.map_id
trace_eq_sum_roots 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map CommSemiring.toSemiring Semifield.toCommSemiring algebraMap minpoly EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike LinearMap CommRing.toCommSemiring RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule LinearMap.instFunLike Algebra.trace AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.finrank IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet IntermediateField.toField IntermediateField.instModuleSubtypeMem Multiset.sum Polynomial.aroots instIsDomain	—	instIsDomain IsScalarTower.left trace_eq_trace_adjoin Algebra.smul_def map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots IsScalarTower.algebraMap_smul AddCommMonoid.nat_isScalarTower
trace_eq_trace_adjoin 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule LinearMap.instFunLike Algebra.trace AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Module.finrank IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IntermediateField.toField IntermediateField.instModuleSubtypeMem IntermediateField.algebra' Algebra.toSMul Semifield.toCommSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IntermediateField.AdjoinSimple.gen	—	IsScalarTower.left Algebra.trace_trace IntermediateField.isScalarTower_mid' Module.Free.of_divisionRing IntermediateField.finiteDimensional_left IntermediateField.finiteDimensional_right SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IntermediateField.AdjoinSimple.algebraMap_gen Algebra.trace_algebraMap commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul AddCommMonoid.nat_isScalarTower IsScalarTower.right

---

← Back to Index