Defs

📁 Source: Mathlib/FieldTheory/Normal/Defs.lean

Statistics

Metric	Count
Definitions restrictNormal, restrictNormalHom, restrictNormal, restrictNormal', restrictNormalAux, Normal, algHomEquivAut	7
Theorems restrictNormalHom_apply, restrictNormalHom_id, restrictNormal_commutes, restrictNormal_trans, transfer_normal, normal_bijective, restrictNormal_commutes, restrictNormal_comp, restrictScalars_normal, restrictNormalHom_comp, restrictNormalHom_comp_apply, algHomEquivAut_apply, algHomEquivAut_symm_apply, isIntegral, of_algEquiv, of_equiv_equiv, out, splits, splits', toIsAlgebraic, tower_top_of_normal, normal_iff, normal_self	23
Total	30

AlgEquiv

Definitions

Name	Category	Theorems
restrictNormal 📖	CompOp	4 math math: restrictNormal_trans, restrict_liftNormal, IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply, restrictNormal_commutes
restrictNormalHom 📖	CompOp	12 math math: InfiniteGalois.normalAutEquivQuotient_apply, FiniteGaloisIntermediateField.mem_fixingSubgroup_iff, restrictNormalHom_surjective, IntermediateField.map_fixingSubgroup, IsScalarTower.AlgEquiv.restrictNormalHom_comp, IsGalois.normalAutEquivQuotient_apply, InfiniteGalois.restrict_fixedField, restrictNormalHom_id, InfiniteGalois.restrictNormalHom_continuous, restrictNormalHom_apply, IsScalarTower.AlgEquiv.restrictNormalHom_comp_apply, IntermediateField.restrictNormalHom_ker

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictNormalHom_apply 📖	mathematical	—	IntermediateField SetLike.instMembership IntermediateField.instSetLike DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule instFunLike MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid aut MonoidHom.instFunLike restrictNormalHom IntermediateField.instAlgebraSubtypeMem IntermediateField.isScalarTower_mid'	—	IsScalarTower.left restrictNormal_commutes IntermediateField.isScalarTower_mid'
restrictNormalHom_id 📖	mathematical	—	restrictNormalHom Algebra.id Semifield.toCommSemiring Field.toSemifield IsScalarTower.right DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidHom.id AlgEquiv MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid aut	—	MonoidHom.ext IsScalarTower.right ext RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing restrictNormal_commutes
restrictNormal_commutes 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap AlgEquiv instFunLike restrictNormal	—	AlgHom.restrictNormal_commutes
restrictNormal_trans 📖	mathematical	—	restrictNormal trans Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	ext RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing restrictNormal_commutes
transfer_normal 📖	mathematical	—	Normal	—	Normal.of_algEquiv

AlgHom

Definitions

Name	Category	Theorems
restrictNormal 📖	CompOp	3 math math: restrictNormal_comp, restrict_liftNormal, restrictNormal_commutes
restrictNormal' 📖	CompOp	1 math math: Normal.algHomEquivAut_apply
restrictNormalAux 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normal_bijective 📖	mathematical	—	Function.Bijective DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring funLike	—	Algebra.IsAlgebraic.bijective_of_isScalarTower' instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Normal.toIsAlgebraic
restrictNormal_commutes 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap AlgHom funLike restrictNormal	—	IsLocalRing.toNontrivial Field.instIsLocalRing AlgEquiv.apply_symm_apply
restrictNormal_comp 📖	mathematical	—	comp Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring restrictNormal	—	ext RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing restrictNormal_commutes

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictScalars_normal 📖	mathematical	—	Normal IntermediateField SetLike.instMembership instSetLike restrictScalars toField algebra' Semifield.toCommSemiring Field.toSemifield Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule	—	IsScalarTower.left

IsScalarTower.AlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictNormalHom_comp 📖	mathematical	—	AlgEquiv.restrictNormalHom MonoidHom.comp AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut	—	MonoidHom.ext AlgEquiv.ext RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing IsScalarTower.algebraMap_eq AlgEquiv.restrictNormal_commutes
restrictNormalHom_comp_apply 📖	mathematical	—	DFunLike.coe MonoidHom AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut MonoidHom.instFunLike AlgEquiv.restrictNormalHom	—	restrictNormalHom_comp MonoidHom.comp_apply

Normal

Definitions

Name	Category	Theorems
algHomEquivAut 📖	CompOp	2 math math: algHomEquivAut_symm_apply, algHomEquivAut_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algHomEquivAut_apply 📖	mathematical	—	DFunLike.coe Equiv AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv EquivLike.toFunLike Equiv.instEquivLike algHomEquivAut AlgHom.restrictNormal' Algebra.id	—	—
algHomEquivAut_symm_apply 📖	mathematical	—	DFunLike.coe Equiv AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm algHomEquivAut AlgHom.comp CommSemiring.toSemiring IsScalarTower.toAlgHom AlgEquiv.toAlgHom	—	—
isIntegral 📖	mathematical	—	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	Algebra.IsIntegral.isIntegral Algebra.IsAlgebraic.isIntegral toIsAlgebraic
of_algEquiv 📖	mathematical	—	Normal	—	normal_iff AlgEquiv.apply_symm_apply minpoly.algEquiv_eq AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap Polynomial.map_map IsIntegral.map IsScalarTower.left AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Polynomial.Splits.map
of_equiv_equiv 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring algebraMap RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass	Normal	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass normal_iff RingEquiv.apply_symm_apply IsIntegral.map_of_comp_eq minpoly.map_eq_of_equiv_equiv instIsDomain Algebra.IsAlgebraic.isIntegral Polynomial.map_map Polynomial.Splits.map
out 📖	mathematical	—	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map CommSemiring.toSemiring Semifield.toCommSemiring algebraMap minpoly	—	normal_iff
splits 📖	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	—	splits'
splits' 📖	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	—	—
toIsAlgebraic 📖	mathematical	—	Algebra.IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	—
tower_top_of_normal 📖	mathematical	—	Normal	—	normal_iff out IsIntegral.tower_top Polynomial.Splits.of_dvd instIsDomain Polynomial.map_map IsScalarTower.algebraMap_eq Polynomial.map_ne_zero DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing minpoly.ne_zero Polynomial.map_dvd_map' minpoly.dvd_map_of_isScalarTower

(root)

Definitions

Name	Category	Theorems
Normal 📖	CompData	31 math math: IntermediateField.normal_inf, IsGalois.to_normal, Normal.of_isSplittingField, IntermediateField.normal_iff_forall_map_eq, IntermediateField.restrictScalars_normal, IntermediateField.AdjoinDouble.normal_algebraicClosure, FixedPoints.normal, IntermediateField.normal_iff_normalClosure_le, IsPurelyInseparable.normal, Normal.of_equiv_equiv, Ideal.Quotient.normal, IntermediateField.normal_iff_forall_fieldRange_le, Algebra.IsQuadraticExtension.normal, AlgEquiv.transfer_normal, IntermediateField.normal_iff_forall_map_le', IntermediateField.normal_iff_forall_fieldRange_eq, IsNormalClosure.normal, Normal.of_algEquiv, normal_iff, IntermediateField.normal_iff_forall_map_le, isGalois_iff, IntermediateField.AdjoinSimple.normal_algebraicClosure, IntermediateField.normal_iff_forall_map_eq', krullTopology_mem_nhds_one_iff_of_normal, IsAlgClosure.normal, normalClosure.normal, normal_self, IntermediateField.normal_sup, IntermediateField.normal_iff_normalClosure_eq, Polynomial.SplittingField.instNormal, Normal.tower_top_of_normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normal_iff 📖	mathematical	—	Normal IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map CommSemiring.toSemiring Semifield.toCommSemiring algebraMap minpoly	—	Normal.isIntegral Normal.splits IsIntegral.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing
normal_self 📖	mathematical	—	Normal Algebra.id Semifield.toCommSemiring Field.toSemifield	—	IsIntegral.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing isIntegral_algebraMap Polynomial.map_sub Polynomial.map_X Polynomial.map_C minpoly.eq_X_sub_C'

---

← Back to Index