IntegralRestrict

📁 Source: Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

Statistics

Metric	Count
Definitions intNorm, intNormAux, intTrace, intTraceAux, galLift, galLiftEquiv, galRestrict, galRestrict', galRestrictHom, instFintypeAlgEquivOfIsDomainOfIsIntegrallyClosedOfFiniteOfIsTorsionFree	10
Theorems algebraMap_intNorm, algebraMap_intNorm_fractionRing, algebraMap_intNorm_of_isGalois, algebraMap_intTrace, algebraMap_intTrace_fractionRing, dvd_algebraMap_intNorm_self, intNorm_eq_norm, intNorm_eq_of_isLocalization, intNorm_eq_zero, intNorm_intNorm, intNorm_map_algEquiv, intNorm_ne_zero, intNorm_zero, intTrace_eq_of_isLocalization, intTrace_eq_trace, map_intNormAux, map_intTraceAux, algebraMap_galRestrict'_apply, algebraMap_galRestrictHom_apply, algebraMap_galRestrict_apply, coe_galRestrict_apply, galLiftEquiv_algebraMap_apply, galLiftEquiv_apply, galLiftEquiv_symm_apply, galLift_algebraMap_apply, galLift_comp, galLift_galRestrict', galLift_id, galRestrict'_comp, galRestrict'_galLift, galRestrict'_id, galRestrictHom_apply, galRestrictHom_symm_algebraMap_apply, galRestrictHom_symm_apply, galRestrict_apply, galRestrict_symm_algebraMap_apply, prod_galRestrict_eq_norm	37
Total	47

Algebra

Definitions

Name	Category	Theorems
intNorm 📖	CompOp	16 math math: Ideal.intNorm_mem_spanNorm, Ideal.map_spanIntNorm, dvd_algebraMap_intNorm_self, algebraMap_intNorm, Ideal.relNorm_singleton, Ideal.map_relNorm, algebraMap_intNorm_fractionRing, intNorm_eq_of_isLocalization, intNorm_eq_norm, intNorm_zero, Ideal.spanNorm_singleton, algebraMap_intNorm_of_isGalois, Ideal.relNorm_apply, intNorm_map_algEquiv, intNorm_intNorm, intNorm_eq_zero
intNormAux 📖	CompOp	1 math math: map_intNormAux
intTrace 📖	CompOp	5 math math: intTrace_eq_of_isLocalization, trace_quotient_eq_of_isDedekindDomain, algebraMap_intTrace, algebraMap_intTrace_fractionRing, intTrace_eq_trace
intTraceAux 📖	CompOp	1 math math: map_intTraceAux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_intNorm 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike intNorm Ring.toSemiring DivisionRing.toRing Field.toDivisionRing EuclideanDomain.toCommRing Field.toEuclideanDomain norm	—	AlgEquiv.injective AlgEquiv.commutes intNorm.eq_1 map_intNormAux IsIntegralClosure.isFractionRing_of_finite_extension norm_eq_of_equiv_equiv FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial RingHom.ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass IsFractionRing.algEquiv_commutes Localization.isLocalization FractionRing.instIsScalarTower IsScalarTower.right OreLocalization.instIsScalarTower IsScalarTower.left
algebraMap_intNorm_fractionRing 📖	mathematical	—	DFunLike.coe RingHom FractionRing Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.instSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra id MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike intNorm Ring.toSemiring OreLocalization.instRing CommRing.toRing OreLocalization.instCommRing norm FractionRing.liftAlgebra FractionRing.field FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial	—	map_intNormAux
algebraMap_intNorm_of_isGalois 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike intNorm IsIntegral.of_finite CommRing.toRing Finset.prod AlgEquiv CommRing.toCommMonoid Finset.univ instFintypeAlgEquivOfIsDomainOfIsIntegrallyClosedOfFiniteOfIsTorsionFree AlgEquiv.instFunLike	—	FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial IsIntegral.of_finite Module.Finite.of_isLocalization OreLocalization.instIsScalarTower IsScalarTower.right FractionRing.instIsScalarTower IsScalarTower.left Localization.isLocalization IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors IsAlgebraic.of_finite IsDomain.to_noZeroDivisors IsIntegralClosure.of_isIntegrallyClosed IsSeparable.isAlgebraic FractionRing.instNontrivial IsGalois.to_isSeparable Equiv.prod_comp Finset.prod_congr IsPurelyInseparable.isIntegral isPurelyInseparable_self isIntegral_norm IsIntegral.algebraMap IsIntegralClosure.isIntegral IsLocalRing.toNontrivial Field.instIsLocalRing prod_galRestrict_eq_norm
algebraMap_intTrace 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instFunLike intTrace EuclideanDomain.toCommRing Field.toEuclideanDomain trace	—	AlgEquiv.injective AlgEquiv.commutes intTrace.eq_1 map_intTraceAux IsIntegralClosure.isFractionRing_of_finite_extension trace_eq_of_equiv_equiv FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial RingHom.ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass IsFractionRing.algEquiv_commutes Localization.isLocalization FractionRing.instIsScalarTower IsScalarTower.right OreLocalization.instIsScalarTower IsScalarTower.left
algebraMap_intTrace_fractionRing 📖	mathematical	—	DFunLike.coe RingHom FractionRing Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.instSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra id LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instFunLike intTrace OreLocalization.instCommRing FractionRing.liftAlgebra FractionRing.field FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul CommRing.toRing IsDomain.toIsCancelMulZero IsDomain.toNontrivial trace	—	map_intTraceAux
dvd_algebraMap_intNorm_self 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike intNorm IsIntegral.of_finite CommRing.toRing	—	IsIntegral.of_finite intNorm_zero Module.Finite.of_isLocalization FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial OreLocalization.instIsScalarTower IsScalarTower.right FractionRing.instIsScalarTower IsScalarTower.left Localization.isLocalization IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors IsAlgebraic.of_finite IsDomain.to_noZeroDivisors map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one AlgebraicClosure.instIsScalarTower isIntegral_algHom_iff FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing IsScalarTower.coe_toAlgHom' map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_inv₀ IsScalarTower.algebraMap_apply algebraMap_intNorm IsIntegralClosure.of_isIntegrallyClosed instIsDomain norm_eq_prod_roots IsAlgClosed.splits AlgebraicClosure.isAlgClosed Multiset.prod_erase DivisionRing.isSimpleRing Polynomial.eval_map_algebraMap minpoly.ne_zero FractionRing.instNontrivial IsIntegral.isIntegral IsAlgebraic.isIntegral Polynomial.aeval_algebraMap_apply minpoly.aeval Module.IsTorsionFree.trans_faithfulSMul Module.Free.self instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors mul_pow mul_pow_sub_one Module.finrank_pos commRing_strongRankCondition SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IntermediateField.finiteDimensional_right mul_assoc inv_mul_cancel_left₀ map_ne_zero_iff IsIntegral.mul IsIntegral.pow isIntegral_algebraMap_iff Module.isTorsionFree_iff_algebraMap_injective IsIntegral.multiset_prod minpoly.monic Multiset.erase_subset minpoly.isIntegrallyClosed_eq_field_fractions Polynomial.aeval_map_algebraMap IsIntegrallyClosed.isIntegral_iff IsIntegral.tower_top mul_inv_cancel_left₀
intNorm_eq_norm 📖	mathematical	—	intNorm norm CommRing.toRing	—	MonoidHom.ext IsFractionRing.injective Localization.isLocalization FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial algebraMap_intNorm_fractionRing norm_localization IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors Module.Free.instFaithfulSMulOfNontrivial IsAlgebraic.of_finite IsDomain.to_noZeroDivisors FractionRing.instIsScalarTower IsScalarTower.right OreLocalization.instIsScalarTower IsScalarTower.left
intNorm_eq_of_isLocalization 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike intNorm	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero Unique.instSubsingleton mem_nonZeroDivisors_iff_ne_zero Localization.isLocalization IsScalarTower.right IsScalarTower.of_algebraMap_eq' RingHom.algebraMap_toAlgebra IsLocalization.map_comp RingHomCompTriple.comp_eq RingHomCompTriple.ids IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors IsIntegral.isAlgebraic Submonoid.monotone_map IsLocalization.ringHom_ext RingHom.comp_assoc IsScalarTower.algebraMap_eq RingHom.comp_id FractionRing.instIsScalarTower OreLocalization.instIsScalarTower IsScalarTower.left IsIntegralClosure.of_isIntegrallyClosed IsFractionRing.isFractionRing_of_isDomain_of_isLocalization IsFractionRing.injective IsScalarTower.algebraMap_apply algebraMap_intNorm_fractionRing algebraMap_intNorm
intNorm_eq_zero 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike intNorm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsFractionRing.injective Localization.isLocalization algebraMap_intNorm_fractionRing map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass instIsDomain Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
intNorm_intNorm 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike intNorm	—	FaithfulSMul.algebraMap_injective FractionRing.instFaithfulSMul Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsDomain.toNontrivial Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero algebraMap_intNorm_fractionRing norm_norm Module.Free.of_divisionRing IsDomain.to_noZeroDivisors FractionRing.instIsScalarTower_1 FractionRing.instIsScalarTower IsScalarTower.right OreLocalization.instIsScalarTower
intNorm_map_algEquiv 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike intNorm AlgEquiv AlgEquiv.instFunLike	—	FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.self algebraMap_intNorm_fractionRing Localization.isLocalization FractionRing.instIsScalarTower IsScalarTower.right OreLocalization.instIsScalarTower IsScalarTower.left IsIntegralClosure.of_isIntegrallyClosed galLiftEquiv_algebraMap_apply norm_eq_of_algEquiv
intNorm_ne_zero 📖	—	—	—	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero
intNorm_zero 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike intNorm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsFractionRing.injective Localization.isLocalization algebraMap_intNorm_fractionRing map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass norm_zero FractionRing.instNontrivial Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
intTrace_eq_of_isLocalization 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instFunLike intTrace	—	Unique.instSubsingleton mem_nonZeroDivisors_iff_ne_zero IsDomain.to_noZeroDivisors IsDomain.toNontrivial IsIntegralClosure.of_isIntegrallyClosed Localization.isLocalization OreLocalization.instIsScalarTower IsScalarTower.right IsIntegral.of_finite IsIntegralClosure.isLocalization FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero FractionRing.instIsScalarTower IsScalarTower.left isAlgebraic_of_isFractionRing IsScalarTower.of_algebraMap_eq' RingHom.algebraMap_toAlgebra IsLocalization.map_comp RingHomCompTriple.comp_eq RingHomCompTriple.ids Submonoid.monotone_map IsLocalization.ringHom_ext RingHom.comp_assoc IsScalarTower.algebraMap_eq RingHom.comp_id Module.Finite.of_isLocalization IsFractionRing.isFractionRing_of_isDomain_of_isLocalization IsFractionRing.injective IsScalarTower.algebraMap_apply algebraMap_intTrace_fractionRing algebraMap_intTrace
intTrace_eq_trace 📖	mathematical	—	intTrace trace	—	LinearMap.ext IsFractionRing.injective Localization.isLocalization FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial algebraMap_intTrace_fractionRing trace_localization IsIntegralClosure.isLocalization Module.Free.instFaithfulSMulOfNontrivial FractionRing.instIsScalarTower IsScalarTower.right OreLocalization.instIsScalarTower IsScalarTower.left IsIntegralClosure.of_isIntegrallyClosed IsIntegral.of_finite isAlgebraic_of_isFractionRing
map_intNormAux 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike intNormAux Ring.toSemiring DivisionRing.toRing Field.toDivisionRing EuclideanDomain.toCommRing Field.toEuclideanDomain norm	—	IsIntegralClosure.algebraMap_mk'
map_intTraceAux 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instFunLike intTraceAux EuclideanDomain.toCommRing Field.toEuclideanDomain trace	—	IsIntegralClosure.algebraMap_equiv integralClosure.isIntegralClosure IsIntegralClosure.of_isIntegrallyClosed IsScalarTower.left IsPurelyInseparable.isIntegral isPurelyInseparable_self IsScalarTower.subalgebra' IsScalarTower.right

(root)

Definitions

Name	Category	Theorems
galLift 📖	CompOp	8 math math: galLift_algebraMap_apply, galLift_comp, galLiftEquiv_apply, galLiftEquiv_symm_apply, galLift_galRestrict', galLift_id, galRestrict'_galLift, galRestrictHom_symm_apply
galLiftEquiv 📖	CompOp	3 math math: galLiftEquiv_apply, galLiftEquiv_symm_apply, galLiftEquiv_algebraMap_apply
galRestrict 📖	CompOp	9 math math: galRestrict_symm_algebraMap_apply, Ideal.exists_comap_galRestrict_eq, Ideal.coe_smul_primesOver_mk_eq_map_galRestrict, coe_galRestrict_apply, algebraMap_galRestrict_apply, groupCohomology.exists_mul_galRestrict_of_norm_eq_one, galRestrict_apply, Ideal.coe_smul_primesOver_eq_map_galRestrict, prod_galRestrict_eq_norm
galRestrict' 📖	CompOp	6 math math: galRestrict'_id, galLift_galRestrict', galRestrict'_galLift, galRestrict'_comp, algebraMap_galRestrict'_apply, galRestrictHom_apply
galRestrictHom 📖	CompOp	6 math math: coe_galRestrict_apply, galRestrictHom_symm_algebraMap_apply, galRestrict_apply, galRestrictHom_symm_apply, galRestrictHom_apply, algebraMap_galRestrictHom_apply
instFintypeAlgEquivOfIsDomainOfIsIntegrallyClosedOfFiniteOfIsTorsionFree 📖	CompOp	1 math math: Algebra.algebraMap_intNorm_of_isGalois

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_galRestrict'_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap AlgHom AlgHom.funLike galRestrict' Semifield.toCommSemiring	—	AlgHomClass.toRingHomClass AlgHom.algHomClass IsIntegralClosure.algebraMap_equiv RingHomCompTriple.comp_eq RingHomCompTriple.right_ids
algebraMap_galRestrictHom_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap AlgHom AlgHom.funLike MulEquiv Semifield.toCommSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass AlgHom.End EquivLike.toFunLike MulEquiv.instEquivLike galRestrictHom	—	algebraMap_galRestrict'_apply
algebraMap_galRestrict_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap AlgEquiv AlgEquiv.instFunLike MulEquiv Semifield.toCommSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike galRestrict	—	algebraMap_galRestrictHom_apply
coe_galRestrict_apply 📖	mathematical	—	AlgHomClass.toAlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass DFunLike.coe MulEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike galRestrict AlgHom AlgHom.End galRestrictHom	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
galLiftEquiv_algebraMap_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike galLiftEquiv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	galLift_algebraMap_apply AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
galLiftEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike galLiftEquiv AlgHom AlgHom.funLike galLift AlgHomClass.toAlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	—	—
galLiftEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike AlgEquiv.symm galLiftEquiv AlgHom AlgHom.funLike galLift AlgHomClass.toAlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	—	—
galLift_algebraMap_apply 📖	mathematical	—	DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom.funLike galLift RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	IsLocalization.lift_eq
galLift_comp 📖	mathematical	—	galLift AlgHom.comp CommRing.toCommSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	Function.Injective.isDomain instIsDomain RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsFractionRing.injective IsIntegralClosure.isLocalization AlgHom.coe_ringHom_injective IsLocalization.ringHom_ext AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.ext galLift_algebraMap_apply
galLift_galRestrict' 📖	mathematical	—	galLift galRestrict'	—	Function.Injective.isDomain instIsDomain RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsFractionRing.injective IsIntegralClosure.isLocalization AlgHom.coe_ringHom_injective IsLocalization.ringHom_ext AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.ext AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass IsLocalization.lift_comp IsIntegralClosure.algebraMap_equiv RingHomCompTriple.comp_eq RingHomCompTriple.right_ids
galLift_id 📖	mathematical	—	galLift AlgHom.id CommRing.toCommSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	AlgHom.ext RingHomCompTriple.comp_eq RingHomCompTriple.ids IsLocalization.lift.congr_simp IsLocalization.lift_id
galRestrict'_comp 📖	mathematical	—	galRestrict' AlgHom.comp Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring CommRing.toCommSemiring CommSemiring.toSemiring	—	AlgHom.ext AlgEquiv.injective integralClosure.isIntegralClosure IsScalarTower.subalgebra' IsScalarTower.right AlgEquiv.symm_apply_apply AlgHomClass.toRingHomClass AlgHom.algHomClass IsIntegralClosure.algebraMap_equiv RingHomCompTriple.comp_eq RingHomCompTriple.right_ids
galRestrict'_galLift 📖	mathematical	—	galRestrict' galLift	—	Function.Injective.isDomain instIsDomain RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsFractionRing.injective IsIntegralClosure.isLocalization AlgHom.ext IsIntegralClosure.algebraMap_injective IsIntegralClosure.algebraMap_equiv AlgHomClass.toRingHomClass AlgHom.algHomClass RingHomCompTriple.comp_eq RingHomCompTriple.right_ids IsLocalization.lift_eq
galRestrict'_id 📖	mathematical	—	galRestrict' AlgHom.id Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring CommRing.toCommSemiring CommSemiring.toSemiring	—	AlgHom.ext IsIntegralClosure.algebraMap_injective algebraMap_galRestrict'_apply
galRestrictHom_apply 📖	mathematical	—	DFunLike.coe MulEquiv AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring CommRing.toCommSemiring CommSemiring.toSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass AlgHom.End EquivLike.toFunLike MulEquiv.instEquivLike galRestrictHom galRestrict'	—	—
galRestrictHom_symm_algebraMap_apply 📖	mathematical	—	DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom.funLike MulEquiv CommRing.toCommSemiring CommSemiring.toSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass AlgHom.End EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm galRestrictHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	galLift_algebraMap_apply
galRestrictHom_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv AlgHom CommRing.toCommSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass AlgHom.End EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm galRestrictHom galLift	—	—
galRestrict_apply 📖	mathematical	—	DFunLike.coe AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv.instFunLike MulEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike galRestrict AlgHom AlgHom.funLike AlgHom.End galRestrictHom AlgHomClass.toAlgHom AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	—	—
galRestrict_symm_algebraMap_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike MulEquiv CommRing.toCommSemiring CommSemiring.toSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm galRestrict RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	galRestrictHom_symm_algebraMap_apply AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
prod_galRestrict_eq_norm 📖	mathematical	—	Finset.prod AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring CommRing.toCommMonoid Finset.univ AlgEquiv.fintype DFunLike.coe CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv.instFunLike MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike galRestrict Algebra.IsSeparable.isAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing IsLocalRing.toNontrivial Field.instIsLocalRing IsGalois.to_isSeparable RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap IsIntegralClosure.mk' IsIntegralClosure.of_isIntegrallyClosed Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule IsPurelyInseparable.isIntegral CommRing.toRing isPurelyInseparable_self MonoidHom MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring MonoidHom.instFunLike Algebra.norm Algebra.isIntegral_norm IsIntegral.algebraMap IsIntegralClosure.isIntegral	—	IsIntegralClosure.algebraMap_injective Algebra.IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing IsGalois.to_isSeparable IsIntegralClosure.of_isIntegrallyClosed IsScalarTower.left IsPurelyInseparable.isIntegral isPurelyInseparable_self Algebra.isIntegral_norm IsIntegral.algebraMap IsIntegralClosure.isIntegral IsScalarTower.algebraMap_apply IsScalarTower.algebraMap_eq map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finset.prod_congr algebraMap_galRestrict_apply IsIntegralClosure.algebraMap_mk' Algebra.norm_eq_prod_automorphisms

---

← Back to Index