Documentation Verification Report

QuasiFinite

📁 Source: Mathlib/RingTheory/Etale/QuasiFinite.lean

Statistics

Metric	Count
Definitions `fiberIsoOfBijectiveResidueField`	1
Theorems `exists_etale_isIdempotentElem_forall_liesOver_eq`, `exists_etale_isIdempotentElem_forall_liesOver_eq_aux`, `exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂`, `exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver`, `comap_fiberIsoOfBijectiveResidueField_apply`, `comap_fiberIsoOfBijectiveResidueField_symm`, `eq_of_comap_eq_comap_of_bijective_residueFieldMap`, `exists_finite_awayMapₐ_of_surjective_awayMapₐ`	8
Total	9

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_etale_isIdempotentElem_forall_liesOver_eq` 📖	mathematical	—	`Ideal.comap` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `CommSemiring.toSemiring` `RingHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.instSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `TensorProduct.instAlgebra` `TensorProduct.includeRight` `RingHom.instRingHomClass` `Ideal` `SetLike.instMembership` `Submodule.setLike` `Semiring.toModule` `Function.Bijective` `Ideal.ResidueField` `DFunLike.coe` `AlgHom` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `id` `AlgHom.funLike` `Ideal.ResidueField.mapₐ` `ofId` `Ideal.over_def` `Module.Finite` `Localization.Away` `CommRing.toCommMonoid` `TensorProduct.instCommRing` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `Submonoid.powers` `TensorProduct.addCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `OreLocalization.instModuleOfIsScalarTower` `TensorProduct.leftModule` `to_smulCommClass` `IsScalarTower.right` `TensorProduct.leftAlgebra`	—	`to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass` `RingHom.instRingHomClass` `Ideal.over_def` `exists_etale_isIdempotentElem_forall_liesOver_eq_aux` `ZariskisMainProperty.of_finiteType` `OreLocalization.instIsScalarTower` `exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂` `integralClosure.AlgebraIsIntegral` `IsScalarTower.subalgebra'` `IsLocalization.isPrime_of_isPrime_disjoint` `Localization.isLocalization` `Ideal.disjoint_powers_iff_notMem` `Ideal.IsPrime.isRadical` `IsLocalization.comap_map_of_isPrime_disjoint` `OreLocalization.instSMulCommClass` `IsScalarTower.of_algebraMap_eq'` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `algebraMapSubmonoid_powers` `IsLocalization.Away.eq_1` `IsLocalization.tensorProduct_tensorProduct` `RingHom.ext` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Ideal.LiesOver.trans` `Ideal.IsPrime.under` `PrimeSpectrum.localization_comap_injective` `PrimeSpectrum.ext` `Etale.instAway` `IsIdempotentElem.map` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `Ideal.under.eq_1` `Ideal.comap_comap` `RingHom.SurjectiveOnStalks.residueFieldMap_bijective` `RingHom.surjectiveOnStalks_of_isLocalization` `AlgHom.coe_comp` `Ideal.ResidueField.algHom_ext` `ext_id` `IsLocalRing.instIsScalarTowerResidueField` `Function.Bijective.comp` `TensorProduct.isScalarTower_left` `Ideal.under_liesOver_of_liesOver`
`exists_etale_isIdempotentElem_forall_liesOver_eq_aux` 📖	mathematical	—	`Ideal.comap` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `CommSemiring.toSemiring` `RingHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.instSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `TensorProduct.instAlgebra` `TensorProduct.includeRight` `RingHom.instRingHomClass` `Ideal` `SetLike.instMembership` `Submodule.setLike` `Semiring.toModule` `Function.Bijective` `Ideal.ResidueField` `DFunLike.coe` `AlgHom` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `id` `AlgHom.funLike` `Ideal.ResidueField.mapₐ` `ofId` `Ideal.over_def` `Subalgebra` `Subalgebra.instSetLike` `integralClosure` `Subalgebra.toSemiring` `Subalgebra.algebra` `TensorProduct.leftAlgebra` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `TensorProduct.map` `AlgHom.id` `Subalgebra.val`	—	`to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass` `RingHom.instRingHomClass` `Ideal.over_def` `exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver` `Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd` `Polynomial.Monic.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.Monic.map` `minpoly.monic` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `sub_zero` `Polynomial.leadingCoeff_mul` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.Monic.leadingCoeff` `one_mul` `Polynomial.Monic.mul` `Polynomial.monic_X` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `Irreducible.coprime_iff_not_dvd` `IsBezout.of_isPrincipalIdealRing` `EuclideanDomain.to_principal_ideal_domain` `Prime.irreducible` `Polynomial.instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsDomain.toIsCancelMulZero` `Polynomial.prime_X` `Polynomial.map_mul` `Polynomial.map_X` `pow_succ'` `mul_assoc` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X` `minpoly.aeval` `MulZeroClass.mul_zero` `exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime` `Polynomial.Monic.pow` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `Polynomial.aeval_algHom_apply` `AlgHomClass.toRingHomClass` `eq_sub_iff_add_eq` `mul_sub` `mul_one` `mul_mul_mul_comm` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `Polynomial.aeval_map_algebraMap` `TensorProduct.isScalarTower_left` `IsIdempotentElem.map` `Ideal.comap_fiberIsoOfBijectiveResidueField_symm` `Eq.le` `Ideal.primesOver.isPrime` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `Ideal.primesOver.liesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap` `IsLocalRing.ResidueField.instIsScalarTower` `Localization.AtPrime.instIsScalarTower` `Polynomial.map_pow` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `isReduced_of_noZeroDivisors` `Ideal.IsPrime.mul_mem_left_iff` `Ideal.instIsTwoSided_1` `Submodule.addSubmonoidClass` `Ideal.mul_mem_left` `Ideal.one_notMem` `map_one` `MonoidHomClass.toOneHomClass` `Submodule.sub_mem_iff_left` `eq_sub_iff_add_eq'` `Ideal.comap_liesOver` `Ideal.eq_of_comap_eq_comap_of_bijective_residueFieldMap` `Ideal.IsPrime.comap` `Ideal.comap.congr_simp` `RingHomClass.toRingHom.congr_simp` `TensorProduct.map_restrictScalars_comp_includeRight` `Mathlib.Tactic.Contrapose.contrapose₂` `AlgHom.comp_algebraMap_of_tower` `Subalgebra.instIsScalarTowerSubtypeMem` `TensorProduct.isScalarTower` `IsScalarTower.left` `Ideal.algebraMap_residueField_eq_zero` `Polynomial.aeval_algebraMap_apply` `Polynomial.eval_map_algebraMap` `mul_comm` `AlgHom.comp_algebraMap` `Polynomial.map_map` `Polynomial.eval_mul` `Polynomial.eval_pow` `Polynomial.eval_X` `zero_pow` `MulZeroClass.zero_mul`
`exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂` 📖	mathematical	`IsIdempotentElem` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `CommSemiring.toSemiring` `TensorProduct.instMul` `to_smulCommClass` `IsScalarTower.right` `DFunLike.coe` `AlgHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.instSemiring` `TensorProduct.leftAlgebra` `id` `IsScalarTower.to_smulCommClass` `AlgHom.funLike` `TensorProduct.map` `AlgHom.id` `IsScalarTower.toAlgHom` `Ideal.comap` `RingHom` `RingHom.instFunLike` `AlgHom.toRingHom` `TensorProduct.instAlgebra` `TensorProduct.includeRight` `RingHom.instRingHomClass` `Ideal` `SetLike.instMembership` `Submodule.setLike` `Semiring.toModule` `algebraMap` `Localization.Away` `CommSemiring.toCommMonoid` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `Localization.awayMap`	`Module.Finite` `CommRing.toCommMonoid` `Ring.toSemiring` `CommRing.toRing` `OreLocalization.instAlgebra` `TensorProduct.instCommRing` `OreLocalization.instCommRing` `OreLocalization.instIsScalarTower` `Monoid.toMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `toSMul` `ofId` `OreLocalization.instAddCommMonoidOreLocalization` `TensorProduct.addCommMonoid` `OreLocalization.instModuleOfIsScalarTower` `TensorProduct.leftModule` `OreLocalization.instModule` `OreLocalization.instCommSemiring`	—	`to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass` `RingHom.instRingHomClass` `IsIntegral.of_surjective` `IsIntegral.tensorProduct` `OreLocalization.instIsScalarTower` `IsLocalization.Away.algebraMap_surjective_of_isIdempotentElem` `Localization.isLocalization` `Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐ` `instFiniteTypeAway` `FiniteType.baseChange` `Localization.awayMap_awayMap_surjective` `Localization.awayMap_surjective_iff` `TensorProduct.induction_on` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `MulZeroClass.mul_zero` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `mul_pow` `TensorProduct.tmul_pow` `one_pow` `mul_assoc` `one_mul` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `pow_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Contrapose.contrapose₂` `Ideal.exists_le_maximal` `Iff.not` `Ideal.span_singleton_eq_top` `Ideal.IsPrime.comap` `Ideal.IsMaximal.isPrime'` `Ideal.comap_liesOver` `instLiesOverFiberOfIsPrime` `Ideal.notMem_of_isUnit` `IsLocalization.Away.algebraMap_isUnit` `Eq.le` `Ideal.span_singleton_le_iff_mem` `OreLocalization.instSMulCommClass` `algebraMapSubmonoid_powers` `IsLocalization.Away.eq_1` `IsLocalization.tensorProduct_tensorProduct` `IsScalarTower.of_algHom` `RingHom.ext` `map_one` `MonoidHomClass.toOneHomClass` `IsLocalization.Away.mul` `IsLocalization.Away.mul'` `RingHom.finite_algebraMap` `IsLocalization.ringHom_ext` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `TensorProduct.isScalarTower_left` `AlgHom.comp_algebraMap_of_tower` `RingHom.Finite.comp` `RingEquiv.finite`
`exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Subalgebra` `Subalgebra.instSetLike` `integralClosure` `Subalgebra.toSemiring`	—	`Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver` `EssFiniteType.of_finiteType` `ZariskisMainProperty.of_finiteType` `Localization.isLocalization` `IsLocalization.exists_mk'_eq` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsLocalization.map_mk'` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsLocalization.eq_iff_exists` `Submonoid.mul_mem` `pow_mem` `Submonoid.instSubmonoidClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `Ideal.mul_mem_left` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1` `Ideal.disjoint_powers_iff_notMem` `Ideal.IsPrime.isRadical` `Mathlib.Tactic.Contrapose.contrapose₄` `Ideal.pow_mem_of_mem` `IsLocalization.isPrime_of_isPrime_disjoint` `IsLocalization.comap_map_of_isPrime_disjoint` `Ideal.LiesOver.trans` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Ideal.IsPrime.comap` `Ideal.under.eq_1` `Ideal.comap_comap` `AlgHom.toRingHom_eq_coe` `AlgHom.comp_algebraMap` `Ideal.over_def` `IsScalarTower.subalgebra'` `Ideal.comap_liesOver` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `IsScalarTower.algebraMap_eq` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquiv.commutes` `Ideal.IsPrime.mul_mem_left_iff` `map_pow` `Ideal.notMem_of_isUnit` `IsUnit.pow` `IsLocalization.Away.algebraMap_isUnit` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd`

Ideal

Definitions

Name	Category	Theorems
`fiberIsoOfBijectiveResidueField` 📖	CompOp	2 math math: `comap_fiberIsoOfBijectiveResidueField_apply`, `comap_fiberIsoOfBijectiveResidueField_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_fiberIsoOfBijectiveResidueField_apply` 📖	mathematical	`Function.Bijective` `ResidueField` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `AlgHom.funLike` `ResidueField.mapₐ` `Algebra.ofId` `over_def`	`Ideal` `Set` `Set.instMembership` `primesOver` `OrderIso` `Set.Elem` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.to_smulCommClass` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLikeOrderIso` `fiberIsoOfBijectiveResidueField` `comap` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`	—	`over_def` `Algebra.to_smulCommClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHom.instRingHomClass` `comap.congr_simp` `OrderIso.symm_apply_apply` `comap_fiberIsoOfBijectiveResidueField_symm`
`comap_fiberIsoOfBijectiveResidueField_symm` 📖	mathematical	`Function.Bijective` `ResidueField` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `AlgHom.funLike` `ResidueField.mapₐ` `Algebra.ofId` `over_def`	`comap` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `RingHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.TensorProduct.instSemiring` `RingHom.instFunLike` `RingHomClass.toRingHom` `Algebra.TensorProduct.instAlgebra` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.TensorProduct.includeRight` `RingHom.instRingHomClass` `Ideal` `Set` `Set.instMembership` `primesOver` `Algebra.TensorProduct.leftAlgebra` `Algebra.to_smulCommClass` `OrderIso` `Set.Elem` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Semiring.toModule` `instFunLikeOrderIso` `OrderIso.symm` `fiberIsoOfBijectiveResidueField`	—	`over_def` `ext` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHom.instRingHomClass` `Algebra.to_smulCommClass` `instIsLocalHomAtPrimeRingHomAlgebraMap` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `IsScalarTower.to_smulCommClass` `Algebra.TensorProduct.cancelBaseChange_tmul` `one_smul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `one_mul`
`eq_of_comap_eq_comap_of_bijective_residueFieldMap` 📖	—	`Function.Bijective` `ResidueField` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `AlgHom.funLike` `ResidueField.mapₐ` `Algebra.ofId` `over_def` `comap` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `RingHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.TensorProduct.instSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `RingHom.instRingHomClass`	—	—	`over_def` `Algebra.to_smulCommClass` `RingHom.instRingHomClass` `OrderIso.injective` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `comap_fiberIsoOfBijectiveResidueField_apply`

Localization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finite_awayMapₐ_of_surjective_awayMapₐ` 📖	mathematical	`Away` `CommSemiring.toCommMonoid` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `awayMapₐ` `IsUnit` `Ideal.Fiber` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.TensorProduct.instSemiring` `Ideal.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `IsLocalRing.ResidueField.algebra` `Algebra.id` `TensorProduct.tmul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `Algebra.toModule` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `AlgHom.Finite` `Algebra.ofId`	—	`PrimeSpectrum.isClosedMap_comap_of_isIntegral` `algebraMap_isIntegral_iff` `PrimeSpectrum.isClosed_zeroLocus` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `PrimeSpectrum.isBasis_basic_opens` `IsClosed.isOpen_compl` `PrimeSpectrum.isPrime` `Ideal.IsPrime.ne_top'` `Ideal.eq_top_of_isUnit_mem` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul` `PrimeSpectrum.preimageEquivFiber_apply_asIdeal` `RingHom.finite_iff_isIntegral_and_finiteType` `AlgHom.commutes` `isLocalization` `isIntegral_localization` `IsLocalization.Away.instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap` `IsLocalization.exists_mk'_eq` `instIsConcreteLE` `PrimeSpectrum.basicOpen_eq_zeroLocus_compl` `PrimeSpectrum.preimage_comap_zeroLocus` `Set.image_singleton` `awayMap_surjective_iff` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_pow` `mul_left_comm` `mul_pow` `mul_assoc` `zero_add` `pow_add` `IsLocalization.map.congr_simp` `IsLocalization.mk'.congr_simp` `Function.Surjective.exists` `IsLocalization.mk'_surjective` `IsLocalization.map_mk'` `IsLocalization.eq_iff_exists` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsLocalization.ringHom_ext` `RingHom.ext` `AlgHom.comp_algebraMap_of_tower` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `IsScalarTower.left` `IsLocalization.map_eq` `IsScalarTower.algebraMap_apply` `RingHom.IsIntegral.trans` `RingHom.IsIntegral.of_finite` `RingHom.Finite.of_surjective` `IsScalarTower.of_algebraMap_eq'` `AlgHom.comp_algebraMap` `RingHom.finiteType_algebraMap` `Algebra.FiniteType.of_restrictScalars_finiteType` `instFiniteTypeAway`

---

← Back to Index