Documentation Verification Report

Ideal

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

Statistics

Metric	Count
Definitions `liftₐ`, `map`, `mapₐ`, `instAlgebraQuotientIdealResidueField`	4
Theorems `algHom_ext`, `algHom_ext_iff`, `lift_algebraMap`, `liftₐ_algebraMap`, `liftₐ_comp_toAlgHom`, `map_algebraMap`, `mapₐ_apply`, `ringHom_ext`, `ringHom_ext_iff`, `algebraMap_quotient_residueField_mk`, `algebraMap_residueField_eq_zero`, `algebraMap_residueField_surjective`, `bijective_algebraMap_quotient_residueField`, `injective_algebraMap_quotient_residueField`, `ker_algebraMap_residueField`, `surjectiveOnStalks_residueField`, `residueFieldMap_bijective`, `algebraMap_mk`, `instEssFiniteTypeResidueField`, `instEssFiniteTypeResidueField_1`, `instFiniteResidueField`, `instIsFractionRingQuotientIdealResidueField`, `instIsLocalHomAtPrimeRingHomAlgebraMap`, `instIsScalarTowerQuotientIdealResidueField`, `instLiesOverResidueFieldBotIdeal`	25
Total	29

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_quotient_residueField_mk` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `ResidueField` `Semiring.toNonAssocSemiring` `Quotient.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `algebraMap` `instAlgebraQuotientIdealResidueField` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Quotient.ring` `instIsTwoSided_1` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	`instIsTwoSided_1`
`algebraMap_residueField_eq_zero` 📖	mathematical	—	`DFunLike.coe` `RingHom` `ResidueField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`IsScalarTower.algebraMap_apply` `IsLocalRing.instIsScalarTowerResidueField` `IsScalarTower.right` `IsLocalRing.ResidueField.algebraMap_eq` `IsLocalRing.residue_eq_zero_iff` `IsLocalization.AtPrime.to_map_mem_maximal_iff` `Localization.isLocalization` `IsLocalization.AtPrime.isLocalRing`
`algebraMap_residueField_surjective` 📖	mathematical	—	`ResidueField` `IsMaximal.isPrime'` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	`IsMaximal.isPrime'` `IsScalarTower.algebraMap_eq` `instIsScalarTowerQuotientIdealResidueField` `instIsTwoSided_1` `Function.Bijective.surjective` `bijective_algebraMap_quotient_residueField` `Quotient.mk_surjective`
`bijective_algebraMap_quotient_residueField` 📖	mathematical	—	`Function.Bijective` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `ResidueField` `IsMaximal.isPrime'` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Quotient.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `algebraMap` `instAlgebraQuotientIdealResidueField`	—	`IsMaximal.isPrime'` `injective_algebraMap_quotient_residueField` `IsFractionRing.surjective_iff_isField` `instIsFractionRingQuotientIdealResidueField` `Quotient.isDomain` `instIsTwoSided_1` `Quotient.maximal_ideal_iff_isField_quotient`
`injective_algebraMap_quotient_residueField` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `ResidueField` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Quotient.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `algebraMap` `instAlgebraQuotientIdealResidueField`	—	`RingHom.instRingHomClass` `RingHom.injective_iff_ker_eq_bot` `instIsTwoSided_1` `ker_quotient_lift` `ker_algebraMap_residueField` `map_quotient_self`
`ker_algebraMap_residueField` 📖	mathematical	—	`RingHom.ker` `ResidueField` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	`ext` `RingHom.instRingHomClass` `algebraMap_residueField_eq_zero`
`surjectiveOnStalks_residueField` 📖	mathematical	—	`RingHom.SurjectiveOnStalks` `ResidueField` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `algebraMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	`RingHom.SurjectiveOnStalks.comp` `instIsTwoSided_1` `RingHom.surjectiveOnStalks_of_surjective` `Quotient.mk_surjective` `RingHom.surjectiveOnStalks_of_isLocalization` `Localization.isLocalization`

Ideal.ResidueField

Definitions

Name	Category	Theorems
`liftₐ` 📖	CompOp	2 math math: `liftₐ_comp_toAlgHom`, `liftₐ_algebraMap`
`map` 📖	CompOp	3 math math: `map_algebraMap`, `RingHom.SurjectiveOnStalks.residueFieldMap_bijective`, `mapₐ_apply`
`mapₐ` 📖	CompOp	9 math math: `Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective`, `PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal`, `PrimeSpectrum.preimageEquivFiber_apply_asIdeal`, `Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal`, `PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal`, `Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime`, `Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux`, `mapₐ_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHom_ext` 📖	—	`AlgHom.comp` `Ideal.ResidueField` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `IsScalarTower.toAlgHom` `Algebra.id` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `Algebra.toModule` `IsScalarTower.right` `Algebra.toSMul`	—	—	`IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `AlgHom.coe_ringHom_injective` `ringHom_ext` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`algHom_ext_iff` 📖	mathematical	—	`AlgHom.comp` `Ideal.ResidueField` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `IsScalarTower.toAlgHom` `Algebra.id` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `Algebra.toModule` `IsScalarTower.right` `Algebra.toSMul`	—	`IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `algHom_ext`
`lift_algebraMap` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instPartialOrder` `Ideal.primeCompl` `Submonoid.comap` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsUnit.submonoid`	`DFunLike.coe` `Ideal.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `lift` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	`RingHom.instRingHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `instIsFractionRingQuotientIdealResidueField` `Ideal.instIsTwoSided_1` `lift.eq_1` `IsScalarTower.algebraMap_apply` `instIsScalarTowerQuotientIdealResidueField` `IsLocalization.lift_eq`
`liftₐ_algebraMap` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instPartialOrder` `Ideal.primeCompl` `Submonoid.comap` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsUnit.submonoid`	`DFunLike.coe` `Ideal.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `liftₐ` `RingHom` `RingHom.instFunLike` `algebraMap` `Algebra.id`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `lift_algebraMap`
`liftₐ_comp_toAlgHom` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instPartialOrder` `Ideal.primeCompl` `Submonoid.comap` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsUnit.submonoid`	`AlgHom.comp` `Ideal.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `liftₐ` `IsScalarTower.toAlgHom` `Algebra.id` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.toModule` `IsScalarTower.right` `Algebra.toSMul`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHom.ext` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `liftₐ_algebraMap`
`map_algebraMap` 📖	mathematical	`Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass`	`DFunLike.coe` `Ideal.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `map` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	`RingHom.instRingHomClass` `IsScalarTower.algebraMap_apply` `IsLocalRing.instIsScalarTowerResidueField` `IsScalarTower.right` `Localization.localRingHom_to_map`
`mapₐ_apply` 📖	mathematical	`Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `RingHom.instRingHomClass`	`DFunLike.coe` `AlgHom` `Ideal.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `AlgHom.funLike` `mapₐ` `map`	—	`RingHom.instRingHomClass`
`ringHom_ext` 📖	—	`RingHom.comp` `Ideal.ResidueField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	—	`IsLocalization.ringHom_ext` `instIsFractionRingQuotientIdealResidueField` `Ideal.Quotient.ringHom_ext` `Ideal.instIsTwoSided_1`
`ringHom_ext_iff` 📖	mathematical	—	`RingHom.comp` `Ideal.ResidueField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	`ringHom_ext`

RingHom.SurjectiveOnStalks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`residueFieldMap_bijective` 📖	mathematical	`RingHom.SurjectiveOnStalks` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass`	`Function.Bijective` `Ideal.ResidueField` `DFunLike.coe` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Ideal.ResidueField.map`	—	`RingHom.instRingHomClass` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Ideal.Quotient.lift_surjective_of_surjective` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective`

(root)

Definitions

Name	Category	Theorems
`instAlgebraQuotientIdealResidueField` 📖	CompOp	7 math math: `Ideal.algebraMap_quotient_residueField_mk`, `instIsAlgebraicQuotientIdealResidueField`, `algebraMap_mk`, `Ideal.injective_algebraMap_quotient_residueField`, `instIsScalarTowerQuotientIdealResidueField`, `Ideal.bijective_algebraMap_quotient_residueField`, `instIsFractionRingQuotientIdealResidueField`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_mk` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.ResidueField` `Semiring.toNonAssocSemiring` `Ideal.Quotient.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `algebraMap` `instAlgebraQuotientIdealResidueField` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	—
`instEssFiniteTypeResidueField` 📖	mathematical	—	`Algebra.EssFiniteType` `Ideal.ResidueField` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	`Algebra.EssFiniteType.comp` `IsLocalRing.instIsScalarTowerResidueField` `IsScalarTower.right` `Algebra.instEssFiniteTypeLocalization` `Algebra.EssFiniteType.of_finiteType` `Module.Finite.finiteType` `Module.Finite.self` `IsLocalRing.instFiniteResidueField`
`instEssFiniteTypeResidueField_1` 📖	mathematical	—	`Algebra.EssFiniteType` `Ideal.ResidueField` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap`	—	`Algebra.EssFiniteType.comp` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `instEssFiniteTypeResidueField` `Algebra.EssFiniteType.of_comp` `instIsLocalHomAtPrimeRingHomAlgebraMap` `IsLocalRing.ResidueField.instIsScalarTower` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left`
`instFiniteResidueField` 📖	mathematical	—	`Module.Finite` `Ideal.ResidueField` `Ideal.IsMaximal.isPrime'` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	`Module.Finite.of_surjective` `Ideal.IsMaximal.isPrime'` `RingHomSurjective.ids` `Module.Finite.self` `Ideal.algebraMap_residueField_surjective`
`instIsFractionRingQuotientIdealResidueField` 📖	mathematical	—	`IsFractionRing` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.Quotient.commSemiring` `Ideal.ResidueField` `Semifield.toCommSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `instAlgebraQuotientIdealResidueField`	—	`isUnit_iff_ne_zero` `map_ne_zero_of_mem_nonZeroDivisors` `IsDomain.toNontrivial` `Ideal.instIsTwoSided_1` `Ideal.Quotient.isDomain` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Ideal.injective_algebraMap_quotient_residueField` `IsLocalRing.residue_surjective` `Localization.isLocalization` `IsLocalization.exists_mk'_eq` `mem_nonZeroDivisors_iff_ne_zero` `Ideal.Quotient.noZeroDivisors` `Ideal.Quotient.eq_zero_iff_mem` `IsScalarTower.algebraMap_eq` `IsLocalRing.instIsScalarTowerResidueField` `IsScalarTower.right` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Ideal.Quotient.mk_surjective` `IsScalarTower.algebraMap_apply` `IsLocalization.AtPrime.isLocalRing` `IsLocalization.AtPrime.to_map_mem_maximal_iff` `map_sub` `RingHomClass.toAddMonoidHomClass` `sub_eq_zero` `one_mul`
`instIsLocalHomAtPrimeRingHomAlgebraMap` 📖	mathematical	—	`IsLocalHom` `Localization.AtPrime` `CommRing.toCommSemiring` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `OreLocalization.instCommSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `OreLocalization.instSemiring` `OreLocalization.instMonoid` `CommMonoid.toMonoid` `RingHom.instFunLike` `algebraMap` `Localization.AtPrime.instAlgebraOfLiesOver`	—	`Localization.isLocalHom_localRingHom` `Ideal.over_def`
`instIsScalarTowerQuotientIdealResidueField` 📖	mathematical	—	`IsScalarTower` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.ResidueField` `Submodule.Quotient.instSMul'` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Algebra.toSMul` `IsScalarTower.right` `Ideal.Quotient.commSemiring` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `instAlgebraQuotientIdealResidueField` `DivisionSemiring.toSemiring` `IsLocalRing.ResidueField` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra`	—	`IsScalarTower.of_algebraMap_eq'`
`instLiesOverResidueFieldBotIdeal` 📖	mathematical	—	`Ideal.LiesOver` `CommRing.toCommSemiring` `Ideal.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`RingHom.instRingHomClass` `Ideal.ker_algebraMap_residueField`

---

← Back to Index