Instances

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

Statistics

Metric	Count
Definitions	0
Theorems isSeparable_residueField_iff, instIsAlgebraicQuotientIdealResidueField, instIsAlgebraicResidueFieldOfIsIntegral, instIsSeparableQuotientIdealOfResidueField, instIsSeparableResidueFieldOfQuotientIdeal	5
Total	5

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

(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