NormalClosure

📁 Source: Mathlib/RingTheory/NormalClosure.lean

Statistics

Metric	Count
Definitions NormalClosure, instAlgebraFractionRing, instAlgebraNormalClosure, instAlgebraNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instAlgebraNormalClosure_1, instAlgebraSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instCommRingNormalClosure	7
Theorems instFaithfulSMulNormalClosure, instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, instFiniteNormalClosure, instFiniteNormalClosure_1, instIsDedekindDomainNormalClosure, instIsDomainNormalClosure, instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsGaloisFractionRingNormalClosure, instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsIntegrallyClosedNormalClosure, instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, instIsScalarTowerNormalClosure, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, instIsTorsionFreeNormalClosure, instNontrivialNormalClosure	20
Total	27

Ring

Definitions

Name	Category	Theorems
NormalClosure 📖	CompOp	14 math math: instIsTorsionFreeNormalClosure, instFaithfulSMulNormalClosure, instNontrivialNormalClosure, instIsDedekindDomainNormalClosure, instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsIntegrallyClosedNormalClosure, instFiniteNormalClosure, instIsScalarTowerNormalClosure, instFiniteNormalClosure_1, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, instIsGaloisFractionRingNormalClosure, instIsDomainNormalClosure
instAlgebraFractionRing 📖	CompOp	11 math math: instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, instIsGaloisFractionRingNormalClosure
instAlgebraNormalClosure 📖	CompOp	4 math math: instIsTorsionFreeNormalClosure, instFiniteNormalClosure, instIsScalarTowerNormalClosure, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure
instAlgebraNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure 📖	CompOp	4 math math: instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1
instAlgebraNormalClosure_1 📖	CompOp	5 math math: instFaithfulSMulNormalClosure, instIsScalarTowerNormalClosure, instFiniteNormalClosure_1, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, instIsGaloisFractionRingNormalClosure
instAlgebraSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure 📖	CompOp	5 math math: instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure
instCommRingNormalClosure 📖	CompOp	13 math math: instIsTorsionFreeNormalClosure, instFaithfulSMulNormalClosure, instIsDedekindDomainNormalClosure, instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsIntegrallyClosedNormalClosure, instFiniteNormalClosure, instIsScalarTowerNormalClosure, instFiniteNormalClosure_1, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, instIsGaloisFractionRingNormalClosure, instIsDomainNormalClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulSMulNormalClosure 📖	mathematical	—	FaithfulSMul NormalClosure Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring instCommRingNormalClosure instAlgebraNormalClosure_1	—	faithfulSMul_iff_algebraMap_injective FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero instNontrivialNormalClosure instIsTorsionFreeNormalClosure IsDomain.toNontrivial
instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure 📖	mathematical	—	FaithfulSMul AlgebraicClosure FractionRing FractionRing.field IntermediateField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield instAlgebraFractionRing SetLike.instMembership IntermediateField.instSetLike IntermediateField.normalClosure Algebra.toSMul CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField instAlgebraSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure	—	faithfulSMul_iff_algebraMap_injective AlgebraicClosure.instIsScalarTower IsScalarTower.right FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsDomain.toNontrivial IsDomain.to_noZeroDivisors SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsLocalRing.toNontrivial Field.instIsLocalRing FractionRing.instFaithfulSMul Module.Free.self
instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure 📖	mathematical	—	FiniteDimensional FractionRing AlgebraicClosure FractionRing.field IntermediateField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield instAlgebraFractionRing SetLike.instMembership IntermediateField.instSetLike IntermediateField.normalClosure OreLocalization.instDivisionRingNonZeroDivisors CommRing.toRing IsDomain.toNontrivial CommSemiring.toSemiring CommRing.toCommSemiring IsDomain.to_noZeroDivisors OreLocalization.oreSetComm CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero toAddCommGroup DivisionRing.toRing Field.toDivisionRing IntermediateField.toField Algebra.toModule OreLocalization.instCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring normalClosure.algebra Algebra.id AlgebraicClosure.instIsScalarTower IsScalarTower.right OreLocalization.instSemiring	—	Module.Finite.right AlgebraicClosure.instIsScalarTower IsScalarTower.right IsScalarTower.left normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure normalClosure.is_finiteDimensional instFiniteDimensionalFractionRingOfFinite
instFiniteNormalClosure 📖	mathematical	—	Module.Finite NormalClosure CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingNormalClosure Algebra.toModule instAlgebraNormalClosure	—	IsIntegralClosure.finite Localization.isLocalization AlgebraicClosure.instIsScalarTower IsScalarTower.right instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing IsDedekindRing.toIsNoetherian
instFiniteNormalClosure_1 📖	mathematical	—	Module.Finite NormalClosure CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingNormalClosure Algebra.toModule instAlgebraNormalClosure_1	—	Module.Finite.trans instIsScalarTowerNormalClosure instFiniteNormalClosure
instIsDedekindDomainNormalClosure 📖	mathematical	—	IsDedekindDomain NormalClosure instCommRingNormalClosure	—	integralClosure.isDedekindDomain Localization.isLocalization AlgebraicClosure.instIsScalarTower IsScalarTower.right instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure
instIsDomainNormalClosure 📖	mathematical	—	IsDomain NormalClosure CommSemiring.toSemiring CommRing.toCommSemiring instCommRingNormalClosure	—	instIsDomainSubtypeMemSubalgebraIntegralClosure instIsDomain
instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure 📖	mathematical	—	IsFractionRing NormalClosure CommRing.toCommSemiring instCommRingNormalClosure AlgebraicClosure FractionRing FractionRing.field IntermediateField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield instAlgebraFractionRing SetLike.instMembership IntermediateField.instSetLike IntermediateField.normalClosure SubsemiringClass.toCommSemiring SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing SubfieldClass.toSubringClass IntermediateField.instSubfieldClass instAlgebraNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure	—	integralClosure.isFractionRing_of_finite_extension Localization.isLocalization AlgebraicClosure.instIsScalarTower IsScalarTower.right instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure
instIsGaloisFractionRingNormalClosure 📖	mathematical	—	IsGalois FractionRing FractionRing.field NormalClosure instCommRingNormalClosure instIsDomainNormalClosure instAlgebraFractionRing instAlgebraNormalClosure_1 FaithfulSMul.to_isTorsionFree CommRing.toCommSemiring CommSemiring.toSemiring instFaithfulSMulNormalClosure IsDomain.toNontrivial IsDomain.toIsCancelMulZero	—	IsGalois.of_equiv_equiv AlgebraicClosure.instIsScalarTower IsScalarTower.left instIsDomainNormalClosure FaithfulSMul.to_isTorsionFree instFaithfulSMulNormalClosure IsDomain.toNontrivial IsDomain.toIsCancelMulZero IntermediateField.isAlgebraic_tower_bot IsAlgClosure.isAlgebraic instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors AlgebraicClosure.instIsAlgClosureOfIsAlgebraic Algebra.IsAlgebraic.of_finite FractionRing.instNontrivial instFiniteDimensionalFractionRingOfFinite IsGalois.normalClosure IsSepClosure.isGalois IsSepClosure.of_isAlgClosure_of_perfectField Localization.isLocalization instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure RingHom.ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass IsFractionRing.algEquiv_commutes IsScalarTower.right FractionRing.instIsScalarTower FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul OreLocalization.instIsScalarTower IntermediateField.isScalarTower instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1
instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure 📖	mathematical	—	IsIntegralClosure NormalClosure AlgebraicClosure FractionRing FractionRing.field IntermediateField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield instAlgebraFractionRing SetLike.instMembership IntermediateField.instSetLike IntermediateField.normalClosure CommRing.toCommSemiring instCommRingNormalClosure EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField.toField instAlgebraSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure instAlgebraNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure	—	integralClosure.isIntegralClosure
instIsIntegrallyClosedNormalClosure 📖	mathematical	—	IsIntegrallyClosed NormalClosure instCommRingNormalClosure	—	integralClosure.isIntegrallyClosedOfFiniteExtension Localization.isLocalization AlgebraicClosure.instIsScalarTower IsScalarTower.right instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure
instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure 📖	mathematical	—	IsScalarTower FractionRing AlgebraicClosure FractionRing.field IntermediateField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield instAlgebraFractionRing SetLike.instMembership IntermediateField.instSetLike IntermediateField.normalClosure OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul Algebra.id IsScalarTower.right DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField normalClosure.algebra AlgebraicClosure.instIsScalarTower OreLocalization.instCommSemiring OreLocalization.instSemiring instAlgebraSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure	—	IsScalarTower.of_algebraMap_eq' AlgebraicClosure.instIsScalarTower IsScalarTower.right
instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1 📖	mathematical	—	IsScalarTower FractionRing AlgebraicClosure FractionRing.field IntermediateField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield instAlgebraFractionRing SetLike.instMembership IntermediateField.instSetLike IntermediateField.normalClosure OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul IsScalarTower.right DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField normalClosure.algebra Algebra.id AlgebraicClosure.instIsScalarTower OreLocalization.instCommSemiring OreLocalization.instSemiring IntermediateField.algebra' OreLocalization.instAlgebra FractionRing.instIsScalarTower FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul CommRing.toRing IsDomain.toIsCancelMulZero IsDomain.toNontrivial SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction Algebra.toModule OreLocalization.instIsScalarTower IsScalarTower.left NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsScalarTower.to₁₃₄ IsScalarTower.right AlgebraicClosure.instIsScalarTower FractionRing.instIsScalarTower FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial OreLocalization.instIsScalarTower IsScalarTower.left IntermediateField.isScalarTower normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure
instIsScalarTowerNormalClosure 📖	mathematical	—	IsScalarTower NormalClosure Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring instCommRingNormalClosure instAlgebraNormalClosure instAlgebraNormalClosure_1	—	IsScalarTower.of_algebraMap_eq'
instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure 📖	mathematical	—	IsScalarTower NormalClosure AlgebraicClosure FractionRing FractionRing.field IntermediateField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield instAlgebraFractionRing SetLike.instMembership IntermediateField.instSetLike IntermediateField.normalClosure Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring instCommRingNormalClosure instAlgebraNormalClosure DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField instAlgebraNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure instAlgebraSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsScalarTower.subalgebra' IsScalarTower.right
instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1 📖	mathematical	—	IsScalarTower NormalClosure AlgebraicClosure FractionRing FractionRing.field IntermediateField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield instAlgebraFractionRing SetLike.instMembership IntermediateField.instSetLike IntermediateField.normalClosure Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring instCommRingNormalClosure instAlgebraNormalClosure_1 DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField instAlgebraNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure IntermediateField.algebra' OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Monoid.toMulAction Algebra.id IsScalarTower.right OreLocalization.instAlgebra AlgebraicClosure.instIsScalarTower OreLocalization.instCommSemiring FractionRing.instIsScalarTower FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul CommRing.toRing IsDomain.toIsCancelMulZero IsDomain.toNontrivial SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction Algebra.toModule OreLocalization.instIsScalarTower IsScalarTower.left NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsScalarTower.to₁₃₄ IsScalarTower.right AlgebraicClosure.instIsScalarTower FractionRing.instIsScalarTower FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial OreLocalization.instIsScalarTower IsScalarTower.left instIsScalarTowerNormalClosure instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure
instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure 📖	mathematical	—	IsScalarTower AlgebraicClosure FractionRing FractionRing.field IntermediateField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield instAlgebraFractionRing SetLike.instMembership IntermediateField.instSetLike IntermediateField.normalClosure Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField instAlgebraSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure IntermediateField.algebra' OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Monoid.toMulAction Algebra.id IsScalarTower.right OreLocalization.instAlgebra AlgebraicClosure.instIsScalarTower OreLocalization.instCommSemiring FractionRing.instIsScalarTower FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul CommRing.toRing IsDomain.toIsCancelMulZero IsDomain.toNontrivial SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction Algebra.toModule OreLocalization.instIsScalarTower IsScalarTower.left NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsScalarTower.to₁₂₄ IsScalarTower.right AlgebraicClosure.instIsScalarTower FractionRing.instIsScalarTower FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial OreLocalization.instIsScalarTower IsScalarTower.left instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1 instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure
instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure 📖	mathematical	—	Algebra.IsSeparable FractionRing AlgebraicClosure FractionRing.field IntermediateField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield instAlgebraFractionRing SetLike.instMembership IntermediateField.instSetLike IntermediateField.normalClosure OreLocalization.instCommRing nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.oreSetComm CommRing.toCommMonoid DivisionRing.toRing Field.toDivisionRing IntermediateField.toField normalClosure.algebra Algebra.id AlgebraicClosure.instIsScalarTower OreLocalization.instCommSemiring IsScalarTower.right OreLocalization.instSemiring	—	Algebra.isSeparable_tower_top_of_isSeparable AlgebraicClosure.instIsScalarTower IsScalarTower.left IsScalarTower.right normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure IntermediateField.isSeparable_tower_bot IsSepClosure.isSeparable IsSepClosure.of_isAlgClosure_of_perfectField AlgebraicClosure.instIsAlgClosureOfIsAlgebraic Algebra.IsAlgebraic.of_finite FractionRing.instNontrivial IsDomain.toNontrivial instFiniteDimensionalFractionRingOfFinite
instIsTorsionFreeNormalClosure 📖	mathematical	—	Module.IsTorsionFree NormalClosure CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingNormalClosure Algebra.toModule instAlgebraNormalClosure	—	Subalgebra.instIsTorsionFree FaithfulSMul.to_isTorsionFree instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure IsDomain.toNontrivial IsDomain.toIsCancelMulZero instIsDomain
instNontrivialNormalClosure 📖	mathematical	—	Nontrivial NormalClosure	—	SubsemiringClass.nontrivial Subalgebra.instSubsemiringClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsLocalRing.toNontrivial Field.instIsLocalRing

---

← Back to Index