NormalizedTrace

📁 Source: Mathlib/FieldTheory/NormalizedTrace.lean

Statistics

Metric	Count
Definitions normalizedTrace	1
Theorems normalizedTrace_algebraMap, normalizedTrace_algebraMap_apply, normalizedTrace_algebraMap_apply_eq_self, normalizedTrace_algebraMap_eq_id, normalizedTrace_algebraMap_of_lifts, normalizedTrace_comp_algHom, normalizedTrace_def, normalizedTrace_eq_of_fininteDimensional, normalizedTrace_eq_of_fininteDimensional_apply, normalizedTrace_eq_of_finiteDimensional, normalizedTrace_eq_of_finiteDimensional_apply, normalizedTrace_intermediateField, normalizedTrace_map, normalizedTrace_minpoly, normalizedTrace_ne_zero, normalizedTrace_self, normalizedTrace_self_apply, normalizedTrace_surjective, normalizedTrace_trans, normalizedTrace_trans_apply	20
Total	21

Algebra

Definitions

Name	Category	Theorems
normalizedTrace 📖	CompOp	19 math math: normalizedTrace_map, normalizedTrace_algebraMap_eq_id, normalizedTrace_surjective, normalizedTrace_eq_of_finiteDimensional, normalizedTrace_comp_algHom, normalizedTrace_algebraMap, normalizedTrace_intermediateField, normalizedTrace_eq_of_fininteDimensional, normalizedTrace_algebraMap_apply_eq_self, normalizedTrace_self, normalizedTrace_minpoly, normalizedTrace_eq_of_finiteDimensional_apply, normalizedTrace_algebraMap_apply, normalizedTrace_def, normalizedTrace_trans_apply, normalizedTrace_algebraMap_of_lifts, normalizedTrace_trans, normalizedTrace_eq_of_fininteDimensional_apply, normalizedTrace_self_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normalizedTrace_algebraMap 📖	mathematical	—	LinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids normalizedTrace LinearMap.restrictScalars CommSemiring.toSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.IsScalarTower.compatibleSMul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction linearMap	—	LinearMap.ext RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul' normalizedTrace_algebraMap_apply
normalizedTrace_algebraMap_apply 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule LinearMap.instFunLike normalizedTrace RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	normalizedTrace_map
normalizedTrace_algebraMap_apply_eq_self 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule LinearMap.instFunLike normalizedTrace RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	IsPurelyInseparable.isIntegral isPurelyInseparable_self normalizedTrace_algebraMap_apply IsScalarTower.left normalizedTrace_self
normalizedTrace_algebraMap_eq_id 📖	mathematical	—	LinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toModule toModule RingHom.id RingHomCompTriple.ids normalizedTrace linearMap LinearMap.id	—	LinearMap.ext RingHomCompTriple.ids normalizedTrace_algebraMap_apply_eq_self
normalizedTrace_algebraMap_of_lifts 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Subsemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semiring.toNonAssocSemiring Polynomial.semiring SetLike.instMembership Subsemiring.instSetLike Polynomial.lifts Semifield.toCommSemiring algebraMap minpoly DivisionRing.toRing Field.toDivisionRing	DFunLike.coe RingHom RingHom.instFunLike LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instFunLike normalizedTrace	—	IsIntegral.isIntegral normalizedTrace_minpoly mul_neg map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_inv₀ RingHomClass.toMonoidWithZeroHomClass map_natCast minpoly.map_algebraMap Polynomial.natDegree_map DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.nextCoeff_map_eq
normalizedTrace_comp_algHom 📖	mathematical	—	LinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids normalizedTrace SemilinearMapClass.semilinearMap AlgHom CommSemiring.toSemiring AlgHom.funLike NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass	—	LinearMap.ext RingHomCompTriple.ids NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass normalizedTrace_map
normalizedTrace_def 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule LinearMap.instFunLike normalizedTrace toSMul CommSemiring.toSemiring id InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Module.finrank IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet IntermediateField.toField IntermediateField.module' IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toCommSemiring IntermediateField.algebra' trace IntermediateField.AdjoinSimple.gen	—	—
normalizedTrace_eq_of_fininteDimensional 📖	mathematical	—	normalizedTrace LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul to_smulCommClass Semifield.toCommSemiring Field.toSemifield id InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring trace	—	normalizedTrace_eq_of_finiteDimensional
normalizedTrace_eq_of_fininteDimensional_apply 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule LinearMap.instFunLike normalizedTrace toSMul CommSemiring.toSemiring id InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Module.finrank CommRing.toCommSemiring trace	—	normalizedTrace_eq_of_finiteDimensional_apply
normalizedTrace_eq_of_finiteDimensional 📖	mathematical	—	normalizedTrace LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul to_smulCommClass Semifield.toCommSemiring Field.toSemifield id InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring trace	—	LinearMap.ext to_smulCommClass normalizedTrace_eq_of_finiteDimensional_apply
normalizedTrace_eq_of_finiteDimensional_apply 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule LinearMap.instFunLike normalizedTrace toSMul CommSemiring.toSemiring id InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Module.finrank CommRing.toCommSemiring trace	—	—
normalizedTrace_intermediateField 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule LinearMap.instFunLike normalizedTrace IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField IntermediateField.algebra' toSMul CommSemiring.toSemiring id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IsAlgebraic.isIntegral DivisionRing.toRing Field.toDivisionRing IntermediateField.isAlgebraic_tower_bot IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing IsSeparable.of_integral instIsDomain	—	—
normalizedTrace_map 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule LinearMap.instFunLike normalizedTrace AlgHom AlgHom.funLike	—	—
normalizedTrace_minpoly 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule LinearMap.instFunLike normalizedTrace toSMul CommSemiring.toSemiring id InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Polynomial.natDegree CommRing.toCommSemiring minpoly NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Polynomial.nextCoeff	—	IsIntegral.isIntegral IsScalarTower.left normalizedTrace_def trace_adjoinSimpleGen IntermediateField.adjoin.finrank
normalizedTrace_ne_zero 📖	—	—	—	—	normalizedTrace_surjective DFunLike.ne_iff one_ne_zero NeZero.charZero_one
normalizedTrace_self 📖	mathematical	—	normalizedTrace id Semifield.toCommSemiring Field.toSemifield IsPurelyInseparable.isIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing isPurelyInseparable_self LinearMap.id DivisionSemiring.toSemiring Semifield.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule	—	LinearMap.ext IsPurelyInseparable.isIntegral isPurelyInseparable_self normalizedTrace_self_apply
normalizedTrace_self_apply 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring id Semiring.toModule LinearMap.instFunLike normalizedTrace IsPurelyInseparable.isIntegral DivisionRing.toRing Field.toDivisionRing isPurelyInseparable_self	—	IsPurelyInseparable.isIntegral isPurelyInseparable_self Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self Module.finrank_self commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Nat.cast_one inv_one one_smul trace_self_apply
normalizedTrace_surjective 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule LinearMap.instFunLike normalizedTrace	—	normalizedTrace_algebraMap_apply_eq_self
normalizedTrace_trans 📖	mathematical	—	LinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids normalizedTrace LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction toSMul IsScalarTower.right	—	LinearMap.ext RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul IsScalarTower.right normalizedTrace_trans_apply
normalizedTrace_trans_apply 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring Semiring.toModule LinearMap.instFunLike normalizedTrace	—	IsScalarTower.left IntermediateField.finiteDimensional_adjoin Finite.of_fintype IsIntegral.isIntegral IsIntegral.tower_top IntermediateField.isScalarTower_mid' IsIntegral.trans IntermediateField.isScalarTower_bot SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IntermediateField.subset_adjoin Subalgebra.range_algebraMap Polynomial.lifts_iff_coeffs_subset_range IsAlgebraic.isIntegral IntermediateField.isAlgebraic_tower_bot IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing IsSeparable.of_integral instIsDomain IntermediateField.charZero normalizedTrace_algebraMap_of_lifts normalizedTrace_algebraMap_apply IntermediateField.isScalarTower_mid

---

← Back to Index