Instances

📁 Source: Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean

Statistics

Metric	Count
Definitions algebraOfIsIntegral	1
Theorems isSeparable_residueField_iff, isScalarTowerOfIsIntegral, instFiniteResidueField_1, instIsAlgebraicQuotientIdealResidueField, instIsAlgebraicResidueFieldOfIsIntegral, instIsSeparableQuotientIdealOfResidueField, instIsSeparableResidueFieldOfQuotientIdeal	7
Total	8

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparable_residueField_iff 📖	mathematical	—	IsSeparable Ideal.ResidueField Ideal.IsMaximal.isPrime' CommRing.toCommSemiring IsLocalRing.instCommRingResidueField Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid DivisionRing.toRing Field.toDivisionRing IsLocalRing.ResidueField.field IsLocalRing.ResidueField.instAlgebra Localization.AtPrime.instAlgebraOfLiesOver instIsLocalHomAtPrimeRingHomAlgebraMap HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Ideal.Quotient.commRing Ideal.Quotient.instRingQuotient Ideal.Quotient.algebraOfLiesOver	—	Ideal.IsMaximal.isPrime' instIsLocalHomAtPrimeRingHomAlgebraMap instIsSeparableQuotientIdealOfResidueField instIsSeparableResidueFieldOfQuotientIdeal

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteResidueField_1 📖	mathematical	—	Module.Finite ResidueField DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring ResidueField.algebraOfIsIntegral Algebra.IsIntegral.of_finite DivisionRing.toRing Field.toDivisionRing	—	Module.Finite.of_equiv_equiv RingHom.instRingHomClass Algebra.IsIntegral.of_finite Ideal.instIsTwoSided_1 eq_maximalIdeal Algebra.ker_algebraMap_isMaximal_of_isIntegral RingHom.ker.eq_1 Ideal.Quotient.ringHom_ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.ext module_finite_of_liesOver Ideal.over_under

IsLocalRing.ResidueField

Definitions

Name	Category	Theorems
algebraOfIsIntegral 📖	CompOp	2 math math: IsLocalRing.instFiniteResidueField_1, isScalarTowerOfIsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isScalarTowerOfIsIntegral 📖	mathematical	—	IsScalarTower IsLocalRing.ResidueField Algebra.toSMul CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field algebra Algebra.id Semifield.toCommSemiring algebraOfIsIntegral	—	IsScalarTower.of_algebraMap_eq

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsAlgebraicQuotientIdealResidueField 📖	mathematical	—	Algebra.IsAlgebraic HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.ResidueField Ideal.Quotient.commRing DivisionRing.toRing Field.toDivisionRing IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid instAlgebraQuotientIdealResidueField	—	IsLocalization.isAlgebraic IsDomain.toNontrivial Ideal.instIsTwoSided_1 Ideal.Quotient.isDomain instIsFractionRingQuotientIdealResidueField
instIsAlgebraicResidueFieldOfIsIntegral 📖	mathematical	—	Algebra.IsAlgebraic Ideal.ResidueField IsLocalRing.instCommRingResidueField Localization.AtPrime CommRing.toCommSemiring OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid DivisionRing.toRing Field.toDivisionRing IsLocalRing.ResidueField.field IsLocalRing.ResidueField.instAlgebra Localization.AtPrime.instAlgebraOfLiesOver instIsLocalHomAtPrimeRingHomAlgebraMap	—	Algebra.IsIntegral.tower_top Ideal.Quotient.isScalarTower_of_liesOver IsScalarTower.left instIsIntegralQuotientIdeal Algebra.IsAlgebraic.extendScalars instIsLocalHomAtPrimeRingHomAlgebraMap IsScalarTower.of_algebraMap_eq Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective AlgHom.map_algebraMap Ideal.Quotient.isScalarTower IsScalarTower.right IsLocalRing.instIsScalarTowerResidueField OreLocalization.instIsScalarTower IsLocalRing.ResidueField.instIsScalarTower Localization.AtPrime.instIsScalarTower Ideal.injective_algebraMap_quotient_residueField Algebra.IsAlgebraic.trans IsScalarTower.of_algebraMap_eq' Ideal.Quotient.noZeroDivisors Algebra.IsIntegral.isAlgebraic IsDomain.toNontrivial Ideal.Quotient.isDomain instIsAlgebraicQuotientIdealResidueField
instIsSeparableQuotientIdealOfResidueField 📖	mathematical	—	Algebra.IsSeparable HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.commRing Ideal.Quotient.instRingQuotient Ideal.Quotient.algebraOfLiesOver	—	Ideal.IsMaximal.isPrime' instIsLocalHomAtPrimeRingHomAlgebraMap Algebra.IsSeparable.of_equiv_equiv RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Ideal.bijective_algebraMap_quotient_residueField RingHom.ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.surjective Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective RingEquiv.injective RingEquiv.symm_apply_apply RingEquiv.apply_symm_apply AlgHom.map_algebraMap Ideal.Quotient.isScalarTower IsScalarTower.right IsLocalRing.instIsScalarTowerResidueField OreLocalization.instIsScalarTower IsLocalRing.ResidueField.instIsScalarTower Localization.AtPrime.instIsScalarTower IsScalarTower.left
instIsSeparableResidueFieldOfQuotientIdeal 📖	mathematical	—	Algebra.IsSeparable Ideal.ResidueField Ideal.IsMaximal.isPrime' CommRing.toCommSemiring IsLocalRing.instCommRingResidueField Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid DivisionRing.toRing Field.toDivisionRing IsLocalRing.ResidueField.field IsLocalRing.ResidueField.instAlgebra Localization.AtPrime.instAlgebraOfLiesOver instIsLocalHomAtPrimeRingHomAlgebraMap	—	Algebra.IsSeparable.of_equiv_equiv Ideal.IsMaximal.isPrime' instIsLocalHomAtPrimeRingHomAlgebraMap RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Ideal.bijective_algebraMap_quotient_residueField Ideal.Quotient.ringHom_ext Ideal.instIsTwoSided_1 RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.ext IsLocalRing.ResidueField.instIsScalarTower Localization.AtPrime.instIsScalarTower IsScalarTower.left AlgHom.map_algebraMap Ideal.Quotient.isScalarTower IsScalarTower.right IsLocalRing.instIsScalarTowerResidueField OreLocalization.instIsScalarTower

---

← Back to Index