Documentation Verification Report

Weakly

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

Statistics

Metric	Count
Definitions `WeaklyQuasiFiniteAt`	1
Theorems `baseChange`, `comap_algEquiv`, `eq_of_le_of_under_eq`, `finite_locoalization`, `finite_residueField`, `instOfQuasiFiniteAt`, `of_algHom_localization`, `of_quasiFiniteAt_residueField`, `of_restrictScalars`, `of_surjectiveOnStalks`, `weaklyQuasiFiniteAt_iff`	11
Total	12

Algebra

Definitions

Name	Category	Theorems
`WeaklyQuasiFiniteAt` 📖	MathDef	9 math math: `WeaklyQuasiFiniteAt.of_restrictScalars`, `WeaklyQuasiFiniteAt.comap_algEquiv`, `WeaklyQuasiFiniteAt.of_quasiFiniteAt_residueField`, `weaklyQuasiFiniteAt_iff`, `WeaklyQuasiFiniteAt.of_algHom_localization`, `WeaklyQuasiFiniteAt.of_surjectiveOnStalks`, `WeaklyQuasiFiniteAt.baseChange`, `Polynomial.not_weaklyQuasiFiniteAt`, `WeaklyQuasiFiniteAt.instOfQuasiFiniteAt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`weaklyQuasiFiniteAt_iff` 📖	mathematical	—	`WeaklyQuasiFiniteAt` `QuasiFinite` `HasQuotient.Quotient` `Localization.AtPrime` `CommRing.toCommSemiring` `Ideal` `OreLocalization.instSemiring` `CommSemiring.toSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Ideal.instHasQuotient_1` `OreLocalization.instCommRing` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `OreLocalization.instAlgebra` `Ideal.under` `Ideal.Quotient.commRing` `Ideal.instAlgebraQuotient`	—	`Ideal.instIsTwoSided_1` `RingHom.instRingHomClass` `Ideal.mk_ker` `sup_of_le_left` `Ideal.comap_map_of_surjective` `Ideal.Quotient.mk_surjective` `Ideal.Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver` `Ideal.over_under` `RingHom.SurjectiveOnStalks.localRingHom_surjective` `RingHom.surjectiveOnStalks_of_surjective` `QuasiFinite.iff_of_algEquiv` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHom.instIsTwoSidedKer` `Ideal.ext` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Localization.isLocalization` `IsLocalization.exists_mk'_eq` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Localization.le_comap_primeCompl_iff` `ge_of_eq` `Localization.localRingHom_mk'` `Function.Surjective.exists` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsScalarTower.algebraMap_eq` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Ideal.map_id`

Algebra.WeaklyQuasiFiniteAt

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.WeaklyQuasiFiniteAt` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`RingHom.instRingHomClass` `Algebra.to_smulCommClass` `IsScalarTower.right` `Submodule.Quotient.smulCommClass` `Ideal.Quotient.isScalarTower` `Ideal.instIsTwoSided_1` `Algebra.TensorProduct.map_surjective` `Ideal.Quotient.mk_surjective` `IsScalarTower.to_smulCommClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.TensorProduct.map_ker` `RingHom.ker_coe_toRingHom` `Ideal.map_coe` `Ideal.Quotient.mkₐ_ker` `Ideal.comap.congr_simp` `AlgHom.comp_algebraMap_of_tower` `IsScalarTower.left` `TensorProduct.isScalarTower` `Ideal.map_map` `sup_eq_left` `AlgHom.comp_algebraMap` `Ideal.map_mono` `Ideal.map_comap_le` `Ideal.map_isPrime_of_surjective` `Eq.trans_le` `Algebra.QuasiFiniteAt.baseChange` `Ideal.Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver` `Ideal.over_under` `Ideal.comap_injective_of_surjective` `Ideal.comap_map_of_surjective` `Ideal.comap_comap` `RingHom.ker_eq_comap_bot` `Ideal.mk_ker` `Algebra.QuasiFinite.trans` `OreLocalization.instIsScalarTower` `TensorProduct.isScalarTower_left` `Algebra.QuasiFinite.instQuotientIdeal` `Algebra.QuasiFinite.instOfFinite` `Module.Finite.self` `RingHom.instIsTwoSidedKer` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Ideal.map_id` `Algebra.QuasiFiniteAt.of_surjectiveOnStalks` `RingEquiv.surjectiveOnStalks` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Ideal.comap_symm`
`comap_algEquiv` 📖	mathematical	—	`Algebra.WeaklyQuasiFiniteAt` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `RingEquiv.toRingHom` `AlgEquiv.toRingEquiv` `RingHom.instRingHomClass` `Ideal.IsPrime.comap`	—	`of_surjectiveOnStalks` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `RingHom.surjectiveOnStalks_of_surjective` `AlgEquiv.surjective` `Ideal.ext` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `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`	—	—	`Ideal.instIsTwoSided_1` `Ideal.map_isPrime_of_surjective` `RingHom.instRingHomClass` `Ideal.Quotient.mk_surjective` `Ideal.mk_ker` `Ideal.map_comap_le` `Algebra.QuasiFiniteAt.eq_of_le_of_under_eq` `Ideal.Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver` `Ideal.over_under` `Ideal.map_mono` `Ideal.under_under` `Ideal.Quotient.isScalarTower` `IsScalarTower.right` `Ideal.comap.congr_simp` `Ideal.comap_map_quotientMk` `sup_of_le_right` `Ideal.comap_map_of_surjective` `sup_of_le_left`
`finite_locoalization` 📖	mathematical	—	`Module.Finite` `Localization.AtPrime` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Semiring.toModule` `OreLocalization.instModuleOfIsScalarTower` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Semifield.toCommSemiring` `IsScalarTower.right`	—	`Algebra.QuasiFinite.of_surjective_algHom` `Ideal.instIsTwoSidedBot` `Ideal.map_bot` `RingHom.instRingHomClass` `Ideal.over_def` `Ideal.instLiesOverBotOfIsPrime` `Algebra.weaklyQuasiFiniteAt_iff` `AlgEquiv.surjective` `Module.Finite.of_quasiFinite` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `FiniteDimensional.finiteDimensional_self`
`finite_residueField` 📖	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`	—	`Ideal.instIsTwoSided_1` `RingHom.instRingHomClass` `Ideal.mk_ker` `sup_of_le_left` `Ideal.comap_map_of_surjective` `Ideal.Quotient.mk_surjective` `Ideal.LiesOver.trans` `Ideal.Quotient.isScalarTower` `IsScalarTower.right` `Module.Finite.of_injective` `Ideal.Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver` `Ideal.over_under` `instIsLocalHomAtPrimeRingHomAlgebraMap` `isNoetherian_of_isNoetherianRing_of_finite` `instIsNoetherianRingOfIsArtinianRing` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `IsLocalRing.ResidueField.finite_of_module_finite` `Algebra.IsIntegral.isLocalHom` `Algebra.IsIntegral.of_finite` `Module.Finite.self` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `Algebra.instFiniteResidueFieldOfQuasiFiniteAt` `IsLocalRing.ResidueField.instIsScalarTower_1` `Localization.AtPrime.instIsScalarTower_1` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial`
`instOfQuasiFiniteAt` 📖	mathematical	—	`Algebra.WeaklyQuasiFiniteAt`	—	`Algebra.weaklyQuasiFiniteAt_iff` `Algebra.QuasiFinite.of_surjective_algHom` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective`
`of_algHom_localization` 📖	mathematical	`Localization.AtPrime` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `OreLocalization.instSemiring` `CommSemiring.toSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `OreLocalization.instAlgebra` `AlgHom.funLike`	`Algebra.WeaklyQuasiFiniteAt`	—	`Algebra.weaklyQuasiFiniteAt_iff` `RingHom.instRingHomClass` `Ideal.map_le_iff_le_comap` `Ideal.comap_comap` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.toRingHom_eq_coe` `AlgHom.comp_algebraMap_of_tower` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `IsScalarTower.left` `le_imp_le_of_le_of_le` `le_refl` `Ideal.le_comap_map` `IsLocalHom.of_surjective` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `IsLocalHom.map_nonunit` `Localization.isLocalization` `AlgHom.commutes` `IsLocalization.mk'_one` `IsLocalization.AtPrime.isUnit_mk'_iff` `Algebra.QuasiFinite.of_surjective_algHom` `Ideal.instIsTwoSided_1` `Ideal.quotientMap_surjective`
`of_quasiFiniteAt_residueField` 📖	mathematical	`Ideal.comap` `Ideal.Fiber` `RingHom` `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` `Algebra.TensorProduct.instSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `RingHom.instRingHomClass`	`Algebra.WeaklyQuasiFiniteAt`	—	`RingHom.instRingHomClass` `Algebra.to_smulCommClass` `Algebra.weaklyQuasiFiniteAt_iff` `Ideal.instIsTwoSided_1` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsLocalization.AtPrime.map_eq_maximalIdeal` `Localization.isLocalization` `Ideal.map_le_iff_le_comap` `Ideal.comap_coe` `Ideal.comap_comap` `Ideal.comap.congr_simp` `IsScalarTower.coe_toAlgHom` `Ideal.le_comap_map` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Ideal.Quotient.isScalarTower` `Commute.all` `Ideal.Fiber.exists_smul_eq_one_tmul` `Submonoid.mul_mem` `Ideal.over_def` `instLiesOverFiberOfIsPrime` `Algebra.smul_def` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsLocalization.map_units` `map_one` `MonoidHomClass.toOneHomClass` `one_mul` `IsUnit.mul_iff` `instIsDedekindFiniteMonoid` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `Ideal.Quotient.mk_surjective` `IsLocalization.exists_mk'_eq` `Ideal.primeCompl.congr_simp` `IsScalarTower.algebraMap_apply` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Algebra.QuasiFinite.trans` `TensorProduct.isScalarTower_left` `Algebra.QuasiFinite.instResidueField` `Algebra.QuasiFinite.instOfFinite` `Module.Finite.self` `Algebra.QuasiFinite.of_surjective_algHom`
`of_restrictScalars` 📖	mathematical	—	`Algebra.WeaklyQuasiFiniteAt`	—	`Ideal.instIsTwoSided_1` `Ideal.Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver` `Ideal.over_under` `Algebra.QuasiFinite.of_restrictScalars` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Ideal.Quotient.isScalarTower` `RingHom.instRingHomClass` `IsScalarTower.algebraMap_eq` `Ideal.comap.congr_simp` `Ideal.map_mono` `Ideal.map_comap_le` `Algebra.QuasiFiniteAt.of_surjectiveOnStalks` `RingHom.surjectiveOnStalks_of_surjective` `Ideal.quotientMap_surjective` `Ideal.comap_injective_of_surjective` `Ideal.Quotient.mk_surjective` `Ideal.comap_comap` `Ideal.comap_map_of_surjective` `Ideal.mk_ker` `sup_of_le_left`
`of_surjectiveOnStalks` 📖	mathematical	`RingHom.SurjectiveOnStalks` `AlgHom.toRingHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal.comap` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`	`Algebra.WeaklyQuasiFiniteAt`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `of_algHom_localization`

---

← Back to Index