Basic

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

Statistics

Metric	Count
Definitions `QuasiFiniteAt`	1
Theorems `baseChange`, `discreteTopology_primeSpectrum`, `eq_of_le_of_under_eq`, `finite_comap_preimage`, `finite_comap_preimage_singleton`, `finite_fiber`, `finite_primeSpectrum`, `finite_primesOver`, `iff_finite_comap_preimage_singleton`, `iff_finite_primesOver`, `iff_of_algEquiv`, `iff_of_isArtinianRing`, `instFiniteResidueField`, `instIsArtinianRingFiber`, `instLocalization`, `instOfFinite`, `instOfIsFractionRing`, `instQuotientIdeal`, `instResidueField`, `isDiscrete_comap_preimage`, `isDiscrete_comap_preimage_singleton`, `of_forall_exists_mul_mem_range`, `of_isIntegral_of_finiteType`, `of_isLocalization`, `of_restrictScalars`, `of_surjective_algHom`, `trans`, `baseChange`, `comap_algEquiv`, `eq_of_le_of_under_eq`, `exists_basicOpen_eq_singleton`, `isClopen_singleton`, `of_isOpen_singleton`, `of_le`, `of_surjectiveOnStalks`, `of_surjectiveOnStalks_of_liesOver`, `instFiniteResidueFieldOfQuasiFiniteAt`, `quasiFinite_iff`, `lift_residueField_surjective`, `exists_not_mem_forall_mem_of_ne_of_liesOver`, `of_quasiFinite`	41
Total	42

Algebra

Definitions

Name	Category	Theorems
`QuasiFiniteAt` 📖	MathDef	12 math math: `QuasiFiniteAt.baseChange`, `QuasiFiniteAt.of_weaklyQuasiFiniteAt`, `QuasiFiniteAt.of_quasiFiniteAt_residueField`, `Polynomial.not_quasiFiniteAt`, `ZariskisMainProperty.quasiFiniteAt`, `quasiFiniteAt_iff_isOpen_singleton_fiber`, `QuasiFiniteAt.of_isOpen_singleton`, `QuasiFiniteAt.of_isOpen_singleton_fiber`, `QuasiFiniteAt.of_le`, `QuasiFiniteAt.of_surjectiveOnStalks_of_liesOver`, `QuasiFiniteAt.of_surjectiveOnStalks`, `QuasiFiniteAt.comap_algEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteResidueFieldOfQuasiFiniteAt` 📖	mathematical	—	`Module.Finite` `Ideal.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `toModule` `Semifield.toCommSemiring` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap`	—	`Localization.AtPrime.isLocalRing` `Ideal.LiesOver.trans` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `IsLocalization.AtPrime.liesOver_maximalIdeal` `Localization.isLocalization` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal` `instIsLocalHomAtPrimeRingHomAlgebraMap` `IsLocalRing.ResidueField.instIsScalarTower_1` `Localization.AtPrime.instIsScalarTower_1` `RingHom.SurjectiveOnStalks.residueFieldMap_bijective` `RingHom.surjectiveOnStalks_of_isLocalization` `Ideal.over_def` `Module.Finite.of_surjective` `RingHomSurjective.ids` `QuasiFinite.instFiniteResidueField` `AlgEquiv.surjective`
`quasiFinite_iff` 📖	mathematical	—	`QuasiFinite`	—	`to_smulCommClass`

Algebra.QuasiFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseChange` 📖	mathematical	—	`Algebra.QuasiFinite` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass` `Ideal.IsPrime.under` `Ideal.over_under` `instIsLocalHomAtPrimeRingHomAlgebraMap` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `IsLocalRing.ResidueField.instIsScalarTower` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `Module.Finite.of_surjective` `RingHomSurjective.ids` `Module.Finite.base_change` `finite_fiber` `AlgEquiv.surjective`
`discreteTopology_primeSpectrum` 📖	mathematical	—	`DiscreteTopology` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology`	—	`isDiscrete_univ_iff` `isDiscrete_comap_preimage`
`eq_of_le_of_under_eq` 📖	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.under`	—	—	`IsDiscrete.eq_of_specializes` `Ideal.IsPrime.under` `isDiscrete_comap_preimage_singleton` `PrimeSpectrum.ext`
`finite_comap_preimage` 📖	mathematical	—	`Set.Finite` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.preimage` `PrimeSpectrum.comap` `algebraMap` `CommSemiring.toSemiring`	—	`Set.Finite.preimage'` `finite_comap_preimage_singleton`
`finite_comap_preimage_singleton` 📖	mathematical	—	`Set.Finite` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.preimage` `PrimeSpectrum.comap` `algebraMap` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet`	—	`PrimeSpectrum.isPrime` `Equiv.finite_iff` `finite_of_compact_of_discrete` `PrimeSpectrum.compactSpace` `PrimeSpectrum.instDiscreteTopology` `instIsArtinianRingFiber`
`finite_fiber` 📖	mathematical	—	`Module.Finite` `Ideal.ResidueField` `Ideal.Fiber` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `Algebra.toModule` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `IsLocalRing.ResidueField`	—	—
`finite_primeSpectrum` 📖	mathematical	—	`Finite` `PrimeSpectrum` `CommRing.toCommSemiring`	—	`Set.finite_univ_iff` `finite_comap_preimage` `Set.finite_univ`
`finite_primesOver` 📖	mathematical	—	`Set.Finite` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.primesOver`	—	`Set.Finite.subset` `Set.Finite.image` `finite_comap_preimage_singleton` `PrimeSpectrum.ext` `Ideal.LiesOver.over` `Ideal.IsPrime.under` `Set.finite_empty`
`iff_finite_comap_preimage_singleton` 📖	mathematical	—	`Algebra.QuasiFinite` `Set.Finite` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.preimage` `PrimeSpectrum.comap` `algebraMap` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet`	—	`finite_comap_preimage_singleton` `Algebra.to_smulCommClass` `Module.finite_iff_isArtinianRing` `Algebra.FiniteType.baseChange` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `FiniteDimensional.finiteDimensional_self` `isArtinianRing_iff_isNoetherianRing_krullDimLE_zero` `isJacobsonRing_of_finiteType` `instIsJacobsonRingOfKrullDimLEOfNatNat` `PrimeSpectrum.instKrullDimLEOfNatNat` `PrimeSpectrum.isPrime` `Equiv.finite_iff` `Algebra.FiniteType.isNoetherianRing` `instIsNoetherianRingOfIsArtinianRing` `PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero` `instDiscreteTopologyOfFiniteOfJacobsonSpace` `PrimeSpectrum.instJacobsonSpaceOfIsJacobsonRing`
`iff_finite_primesOver` 📖	mathematical	—	`Algebra.QuasiFinite` `Set.Finite` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.primesOver`	—	`iff_finite_comap_preimage_singleton` `Equiv.forall_congr_left` `Set.finite_image_iff` `Function.Injective.injOn` `PrimeSpectrum.ext` `Set.ext` `RingHom.instRingHomClass` `Equiv.exists_congr_left`
`iff_of_algEquiv` 📖	mathematical	—	`Algebra.QuasiFinite`	—	`of_surjective_algHom` `AlgEquiv.surjective`
`iff_of_isArtinianRing` 📖	mathematical	—	`Algebra.QuasiFinite` `Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`Module.Finite.of_quasiFinite` `instOfFinite`
`instFiniteResidueField` 📖	mathematical	—	`Module.Finite` `Ideal.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `Algebra.toModule` `Semifield.toCommSemiring` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap`	—	`instIsLocalHomAtPrimeRingHomAlgebraMap` `of_restrictScalars` `IsLocalRing.ResidueField.instIsScalarTower` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `instResidueField` `Module.Finite.of_quasiFinite` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `FiniteDimensional.finiteDimensional_self`
`instIsArtinianRingFiber` 📖	mathematical	—	`IsArtinianRing` `Ideal.Fiber` `Algebra.TensorProduct.instSemiring` `Ideal.ResidueField` `CommRing.toCommSemiring` `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`	—	`IsArtinianRing.of_finite` `Algebra.to_smulCommClass` `IsScalarTower.right` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `FiniteDimensional.finiteDimensional_self` `finite_fiber`
`instLocalization` 📖	mathematical	—	`Algebra.QuasiFinite` `Localization` `CommRing.toCommMonoid` `OreLocalization.instCommRing` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`of_isLocalization` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization`
`instOfFinite` 📖	mathematical	—	`Algebra.QuasiFinite`	—	`Algebra.to_smulCommClass` `Module.Finite.base_change` `Localization.AtPrime.isLocalRing`
`instOfIsFractionRing` 📖	mathematical	—	`Algebra.QuasiFinite`	—	`of_isLocalization` `IsScalarTower.left` `instOfFinite` `Module.Finite.self`
`instQuotientIdeal` 📖	mathematical	—	`Algebra.QuasiFinite` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.Quotient.commRing` `Ideal.instAlgebraQuotient`	—	`of_surjective_algHom` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective`
`instResidueField` 📖	mathematical	—	`Algebra.QuasiFinite` `Ideal.ResidueField` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra`	—	`trans` `instIsScalarTowerQuotientIdealResidueField` `instQuotientIdeal` `instOfIsFractionRing` `instIsFractionRingQuotientIdealResidueField`
`isDiscrete_comap_preimage` 📖	mathematical	`IsDiscrete` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology`	`Set.preimage` `PrimeSpectrum.comap` `algebraMap` `CommSemiring.toSemiring`	—	`IsDiscrete.preimage'` `Continuous.continuousOn` `PrimeSpectrum.continuous_comap` `isDiscrete_comap_preimage_singleton`
`isDiscrete_comap_preimage_singleton` 📖	mathematical	—	`IsDiscrete` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology` `Set.preimage` `PrimeSpectrum.comap` `algebraMap` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet`	—	`Homeomorph.discreteTopology` `PrimeSpectrum.isPrime` `PrimeSpectrum.instDiscreteTopology` `instIsArtinianRingFiber`
`of_forall_exists_mul_mem_range` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `AlgHom.funLike` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Algebra.QuasiFinite`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization` `Submonoid.instSubmonoidClass` `IsLocalization.lift_mk'` `of_surjective_algHom` `instLocalization`
`of_isIntegral_of_finiteType` 📖	mathematical	—	`Algebra.QuasiFinite`	—	`Algebra.subset_adjoin` `Localization.isLocalization` `IsLocalization.Away.algebraMap_isUnit` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `IsScalarTower.of_algebraMap_eq` `IsLocalization.Away.lift_eq` `IsScalarTower.to₁₃₄` `IsScalarTower.subalgebra'` `IsLocalization.exists_mk'_eq` `IsIntegral.tower_top` `IsIntegral.algebraMap` `Algebra.IsIntegral.isIntegral` `IsLocalization.mk'_eq_iff_eq_mul` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Algebra.smul_mul_assoc` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSubsemiringClass` `Localization.mk_eq_mk'` `Algebra.smul_def` `map_one` `MonoidHomClass.toOneHomClass` `one_pow` `one_mul` `mul_pow` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `IsIntegral.smul` `IsScalarTower.left` `Algebra.FiniteType.of_restrictScalars_finiteType` `Algebra.IsIntegral.finite` `Algebra.finite_adjoin_simple_of_isIntegral` `of_isLocalization` `instOfFinite` `trans`
`of_isLocalization` 📖	mathematical	—	`Algebra.QuasiFinite`	—	`trans` `Module.Finite.of_surjective` `Algebra.to_smulCommClass` `RingHomSurjective.ids` `FiniteDimensional.finiteDimensional_self` `LinearMap.IsScalarTower.compatibleSMul'` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `LinearMap.coe_restrictScalars` `LinearMap.range_eq_top` `top_le_iff` `TensorProduct.span_tmul_eq_top` `Submodule.span_le` `IsLocalization.exists_mk'_eq` `IsUnit.mul_left_injective` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsLocalization.map_units` `div_zero` `TensorProduct.zero_tmul` `AlgHom.commutes` `MulZeroClass.mul_zero` `Ideal.instIsTwoSided_1` `map_div₀` `RingHom.instRingHomClass` `RingHomCompTriple.comp_apply` `RingHomCompTriple.right_ids` `div_mul_cancel₀` `mul_one` `smulCommClass_self` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `TensorProduct.tmul_smul` `Algebra.algebraMap_eq_smul_one` `Algebra.mul_smul_comm` `IsLocalization.smul_mk'_self`
`of_restrictScalars` 📖	mathematical	—	`Algebra.QuasiFinite`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `TensorProduct.isScalarTower_left` `TensorProduct.isScalarTower` `Commute.all` `IsScalarTower.to_smulCommClass` `AlgHom.coe_restrictScalars'` `AlgHom.coe_toLinearMap` `RingHomSurjective.ids` `LinearMap.range_eq_top` `top_le_iff` `TensorProduct.span_tmul_eq_top` `Submodule.span_le` `mul_one` `one_mul` `Module.Finite.of_quasiFinite` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `FiniteDimensional.finiteDimensional_self` `baseChange` `Module.Finite.of_surjective`
`of_surjective_algHom` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`Algebra.QuasiFinite`	—	`IsScalarTower.of_algebraMap_eq'` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `Module.Finite.of_surjective` `RingHomSurjective.ids` `Module.Finite.self` `trans` `instOfFinite`
`trans` 📖	mathematical	—	`Algebra.QuasiFinite`	—	`Algebra.to_smulCommClass` `iff_of_isArtinianRing` `instIsArtinianRingFiber` `baseChange` `Algebra.TensorProduct.instSMulCommClassTensorProduct_1` `Module.Finite.trans` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `finite_fiber` `AlgEquiv.map_mul'` `AlgEquiv.map_add'` `IsScalarTower.to_smulCommClass'` `Algebra.TensorProduct.right_isScalarTower` `TensorProduct.smulCommClass_left` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `TensorProduct.isScalarTower` `Algebra.TensorProduct.cancelBaseChange_tmul` `one_smul` `Module.Finite.of_surjective` `RingHomSurjective.ids` `AlgEquiv.surjective`

Algebra.QuasiFiniteAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseChange` 📖	mathematical	`Ideal.comap` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `RingHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.TensorProduct.instSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `RingHom.instRingHomClass`	`Algebra.QuasiFiniteAt` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`RingHom.instRingHomClass` `IsScalarTower.right` `Algebra.to_smulCommClass` `OreLocalization.instIsScalarTower` `TensorProduct.isScalarTower_left` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsScalarTower.algebraMap_apply` `Localization.localRingHom_to_map` `AlgHom.commutes` `Commute.all` `Algebra.TensorProduct.ext` `Algebra.ext_id` `IsScalarTower.to_smulCommClass` `AlgHom.ext` `map_one` `MonoidHomClass.toOneHomClass` `one_mul` `DFunLike.congr_fun` `Algebra.QuasiFinite.of_forall_exists_mul_mem_range` `Algebra.QuasiFinite.baseChange` `Localization.isLocalization` `IsLocalization.exists_mk'_eq` `IsLocalization.map_units`
`comap_algEquiv` 📖	mathematical	—	`Algebra.QuasiFiniteAt` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `RingEquiv.toRingHom` `AlgEquiv.toRingEquiv` `RingHom.instRingHomClass` `Ideal.IsPrime.comap`	—	`of_surjectiveOnStalks` `RingHom.surjectiveOnStalks_of_surjective` `AlgEquiv.surjective` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `Ideal.ext` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.apply_symm_apply`
`eq_of_le_of_under_eq` 📖	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.under`	—	—	`IsLocalization.isPrime_of_isPrime_disjoint` `Localization.isLocalization` `Localization.AtPrime.isLocalRing` `Algebra.QuasiFinite.eq_of_le_of_under_eq` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal` `IsLocalRing.le_maximalIdeal_of_isPrime` `Ideal.under_under` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `RingHom.instRingHomClass` `Ideal.under_def` `IsLocalization.comap_map_of_isPrime_disjoint` `Localization.AtPrime.comap_maximalIdeal`
`exists_basicOpen_eq_singleton` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SetLike.coe` `TopologicalSpace.Opens` `PrimeSpectrum` `PrimeSpectrum.zariskiTopology` `TopologicalSpace.Opens.instSetLike` `PrimeSpectrum.basicOpen` `Set` `Set.instSingletonSet`	—	`IsScalarTower.right` `IsLocalizedModule.map_units` `instIsLocalizedModuleLinearMapOfIsLocalization` `Localization.isLocalization` `one_smul` `Submonoid.one_mem` `Module.Finite.of_quasiFinite` `Module.Finite.of_restrictScalars_finite` `OreLocalization.instIsScalarTower` `IsArtinianRing.of_finite` `Algebra.EssFiniteType.isNoetherianRing` `instIsNoetherianRingOfIsArtinianRing` `Module.finitePresentation_of_finite` `IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentation` `Module.Finite.self` `isLocalizedModule_iff_isLocalization'` `subset_antisymm` `Set.instAntisymmSubset` `Eq.ge` `PrimeSpectrum.localization_away_comap_range` `OrderIso.surjective` `Localization.AtPrime.isLocalRing` `PrimeSpectrum.ext` `RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Ideal.comap_comap` `AlgHom.algHomClass` `AlgEquiv.toAlgHom_toRingHom` `AlgHom.comp_algebraMap` `IsLocalization.AtPrime.comap_maximalIdeal` `IsLocalization.AtPrime.isLocalRing` `Unique.instSubsingleton` `PrimeSpectrum.instKrullDimLEOfNatNat` `Set.singleton_subset_iff`
`isClopen_singleton` 📖	mathematical	—	`IsClopen` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology` `Set` `Set.instSingletonSet`	—	`PrimeSpectrum.isPrime` `isJacobsonRing_of_finiteType` `instIsJacobsonRingOfKrullDimLEOfNatNat` `PrimeSpectrum.instKrullDimLEOfNatNat` `Algebra.FiniteType.isNoetherianRing` `instIsNoetherianRingOfIsArtinianRing` `List.TFAE.out` `PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing` `exists_basicOpen_eq_singleton` `Algebra.EssFiniteType.of_finiteType` `TopologicalSpace.Opens.isOpen`
`of_isOpen_singleton` 📖	mathematical	`IsOpen` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology` `Set` `Set.instSingletonSet`	`Algebra.QuasiFiniteAt` `PrimeSpectrum.asIdeal` `PrimeSpectrum.isPrime`	—	`Algebra.FiniteType.isNoetherianRing` `instIsNoetherianRingOfIsArtinianRing` `isJacobsonRing_of_finiteType` `instIsJacobsonRingOfKrullDimLEOfNatNat` `PrimeSpectrum.instKrullDimLEOfNatNat` `PrimeSpectrum.isPrime` `PrimeSpectrum.isClopen_iff` `List.TFAE.out` `PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing` `Eq.le` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Submonoid.powers_le` `IsLocalization.map_units` `PrimeSpectrum.localization_away_comap_range` `Function.Injective.subsingleton` `Set.injective_codRestrict` `PrimeSpectrum.localization_comap_injective` `Unique.instSubsingleton` `IsLocalization.exists_mk'_eq` `Ideal.exists_le_maximal` `Localization.AtPrime.isLocalRing` `Ideal.IsMaximal.isPrime'` `Eq.ge` `Ideal.mem_span_singleton_self` `RingHom.instRingHomClass` `AlgHom.commutes` `IsLocalization.AtPrime.isUnit_to_map_iff` `IsUnit.mul_right_cancel` `IsUnit.map` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `mul_assoc` `IsUnit.val_inv_mul` `mul_one` `IsLocalization.mk'_spec` `Algebra.FiniteType.of_surjective` `IsLocalization.instFiniteTypeLocalizationOfFGSubtypeMemSubmonoid` `Monoid.powers_fg` `PrimeSpectrum.comap_injective_of_surjective` `Algebra.QuasiFinite.iff_finite_comap_preimage_singleton` `Set.Subsingleton.finite` `Set.subsingleton_of_subsingleton`
`of_le` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Algebra.QuasiFiniteAt`	—	`OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization` `IsLocalization.map_units` `Algebra.QuasiFinite.of_forall_exists_mul_mem_range` `IsLocalization.exists_mk'_eq` `IsScalarTower.coe_toAlgHom` `IsLocalization.lift.congr_simp` `IsLocalization.lift_eq`
`of_surjectiveOnStalks` 📖	mathematical	`RingHom.SurjectiveOnStalks` `AlgHom.toRingHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass`	`Algebra.QuasiFiniteAt`	—	`RingHom.instRingHomClass` `Algebra.QuasiFinite.of_surjective_algHom` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsScalarTower.algebraMap_apply` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.localRingHom_to_map` `AlgHom.commutes`
`of_surjectiveOnStalks_of_liesOver` 📖	mathematical	`RingHom.SurjectiveOnStalks` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`Algebra.QuasiFiniteAt`	—	`of_surjectiveOnStalks` `Ideal.over_def`

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_not_mem_forall_mem_of_ne_of_liesOver` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`PrimeSpectrum.isPrime` `PrimeSpectrum.ext` `over_def` `Algebra.to_smulCommClass` `Algebra.QuasiFiniteAt.baseChange` `Homeomorph.symm_apply_apply` `Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `FiniteDimensional.finiteDimensional_self` `Algebra.EssFiniteType.baseChange` `Fiber.exists_smul_eq_one_tmul` `Eq.ge` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul` `Algebra.smul_def` `IsPrime.mul_mem_left_iff` `instIsTwoSided_1` `RingHom.ker_isPrime` `instIsDomain` `AlgHom.commutes` `IsScalarTower.algebraMap_apply` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `mul_one` `PrimeSpectrum.preimageEquivFiber_apply_asIdeal` `Homeomorph.injective` `Eq.le` `PrimeSpectrum.basicOpen_eq_zeroLocus_compl`

Ideal.Fiber

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_residueField_surjective` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `Ideal.ResidueField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Algebra.toModule` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsLocalRing.ResidueField` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap` `AlgHom.funLike` `Algebra.TensorProduct.lift` `IsLocalRing.ResidueField.instIsScalarTower` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.ofId` `IsScalarTower.toAlgHom` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Algebra.toSMul` `Commute.all` `NonUnitalNonAssocCommSemiring.toCommMagma` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring` `IsLocalRing.instCommRingResidueField`	—	`RingHom.instRingHomClass` `OrderIso.symm_apply_apply` `Algebra.to_smulCommClass` `PrimeSpectrum.isPrime` `Algebra.QuasiFiniteAt.baseChange` `PrimeSpectrum.isClosed_singleton_iff_isMaximal` `IsClopen.isClosed` `Algebra.QuasiFiniteAt.isClopen_singleton` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `FiniteDimensional.finiteDimensional_self` `Algebra.FiniteType.baseChange` `Function.Surjective.of_comp_left` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `instIsLocalHomAtPrimeRingHomAlgebraMap` `IsLocalRing.ResidueField.instIsScalarTower` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `Commute.all` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.coe_toRingHom` `RingHom.coe_comp` `Ideal.IsMaximal.isPrime'` `Algebra.TensorProduct.ringHom_ext` `Ideal.ResidueField.ringHom_ext` `RingHom.ext` `AlgHom.map_algebraMap` `IsScalarTower.algebraMap_apply` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `mul_one` `Ideal.ResidueField.map_algebraMap` `AlgHom.commutes` `one_mul` `Ideal.algebraMap_residueField_surjective` `RingHom.SurjectiveOnStalks.residueFieldMap_bijective` `RingHom.SurjectiveOnStalks.baseChange'` `Ideal.surjectiveOnStalks_residueField`

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_quasiFinite` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`PrimeSpectrum.isPrime` `Pi.isScalarTower` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective` `PrimeSpectrum.instDiscreteTopology` `IsArtinianRing.instFinitePrimeSpectrum` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `of_surjective` `RingHomSurjective.ids` `self` `IsArtinianRing.localization_surjective` `Localization.isLocalization` `Algebra.to_smulCommClass` `Algebra.QuasiFinite.baseChange` `IsArtinianRing.instLocalization` `Localization.AtPrime.isLocalRing` `trans` `TensorProduct.isScalarTower_left` `pi` `AlgEquiv.surjective`

---

← Back to Index