Documentation Verification Report

Finite

📁 Source: Mathlib/RingTheory/RingHom/Finite.lean

Statistics

Metric	Count
Definitions `Finite`	1
Theorems `smul_mem_finsetIntegerMultiple_span`, `of_isLocalization`, `finite_containsIdentities`, `finite_isStableUnderBaseChange`, `finite_localizationPreserves`, `finite_ofLocalizationSpan`, `finite_respectsIso`, `finite_stableUnderComposition`, `localization_away_map_finite`, `instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl`, `instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors`, `multiple_mem_adjoin_of_mem_localization_adjoin`, `multiple_mem_span_of_mem_localization_span`	13
Total	14

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_mem_finsetIntegerMultiple_span` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `SetLike.coe` `Finset` `Finset.instSetLike` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`finsetIntegerMultiple` `Submonoid.map` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Submonoid` `Submonoid.instSetLike` `Submonoid.smul` `Algebra.toSMul`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Algebra.algebraMap_eq_smul_one` `smul_assoc` `finsetIntegerMultiple_image` `Subtype.prop` `Set.isScalarTower` `one_smul` `smulCommClass_self` `Set.smul_mem_smul_set` `RingHomSurjective.ids` `Submodule.map_span` `AlgHom.coe_toLinearMap` `Algebra.linearMap_apply` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Submodule.span_smul` `eq_iff_exists` `Submonoid.smul_def` `Submonoid.coe_mul` `smul_smul` `Algebra.smul_def` `Submodule.smul_mem`

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isLocalization` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule`	—	`Submonoid.le_comap_map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsLocalization.ringHom_ext` `IsLocalization.map_comp` `Finset.coe_image` `span_eq_top_localization_localization`

RingHom

Definitions

Name	Category	Theorems
`Finite` 📖	MathDef	27 math math: `finite_iff_finiteType_of_isJacobsonRing`, `Finite.comp`, `localization_away_map_finite`, `Finite.id`, `AlgebraicGeometry.Scheme.Hom.finite_app`, `finite_localizationPreserves`, `AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop`, `Finite.of_surjective`, `finite_algebraMap`, `surjective_iff_epi_and_finite`, `finite_respectsIso`, `AlgebraicGeometry.IsFinite.SpecMap_iff`, `finite_stableUnderComposition`, `finite_of_algHom_finiteType_of_isJacobsonRing`, `RingEquiv.finite`, `AlgebraicGeometry.IsFinite.finite_app`, `AlgebraicGeometry.finite_appTop_of_universallyClosed`, `Finite.tensorProductMap`, `finite_isStableUnderBaseChange`, `finite_containsIdentities`, `finite_iff_isIntegral_and_finiteType`, `AlgebraicGeometry.isFinite_iff`, `Finite.of_isIntegral_of_finiteType`, `finite_ofLocalizationSpan`, `Finite.codescendsAlong_faithfullyFlat`, `Finite.of_comp_finite`, `IsIntegral.to_finite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_containsIdentities` 📖	mathematical	—	`ContainsIdentities` `Finite`	—	`Finite.id`
`finite_isStableUnderBaseChange` 📖	mathematical	—	`IsStableUnderBaseChange` `Finite`	—	`finite_respectsIso` `Algebra.to_smulCommClass` `Module.Finite.base_change`
`finite_localizationPreserves` 📖	mathematical	—	`LocalizationPreserves` `Finite`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `instRingHomClass` `Submonoid.le_comap_map` `IsScalarTower.of_algebraMap_eq'` `IsLocalization.map_comp` `Algebra.algebraMapSubmonoid.eq_1` `algebraMap_toAlgebra` `Module.Finite.of_isLocalization`
`finite_ofLocalizationSpan` 📖	mathematical	—	`OfLocalizationSpan` `Finite`	—	`ofLocalizationSpan_iff_finite` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `instRingHomClass` `Submonoid.map_powers` `Localization.isLocalization` `Module.Finite.fg_top` `Submodule.span_attach_biUnion` `eq_top_iff` `Submodule.mem_of_span_eq_top_of_smul_pow_mem` `IsScalarTower.right` `multiple_mem_span_of_mem_localization_span` `IsScalarTower.of_algebraMap_eq'` `Submonoid.le_comap_map` `IsLocalization.map_comp` `IsLocalization.smul_mem_finsetIntegerMultiple_span` `OreLocalization.instIsScalarTower` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsScalarTower.algebraMap_apply` `Algebra.smul_def` `Submonoid.smul_def` `le_iSup` `IsLocalization.finsetIntegerMultiple.congr_simp` `pow_add` `smul_smul`
`finite_respectsIso` 📖	mathematical	—	`RespectsIso` `Finite`	—	`StableUnderComposition.respectsIso` `finite_stableUnderComposition` `Finite.of_surjective` `Equiv.surjective`
`finite_stableUnderComposition` 📖	mathematical	—	`StableUnderComposition` `Finite`	—	`Finite.comp`
`localization_away_map_finite` 📖	mathematical	—	`Finite` `IsLocalization.Away.map` `CommRing.toCommSemiring`	—	`LocalizationPreserves.away` `finite_localizationPreserves`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl` 📖	mathematical	—	`Module.Finite` `Localization.AtPrime` `CommRing.toCommSemiring` `Localization` `CommRing.toCommMonoid` `Algebra.algebraMapSubmonoid` `CommSemiring.toSemiring` `Ideal.primeCompl` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `Algebra.toModule` `OreLocalization.instCommSemiring` `instAlgebraLocalizationAlgebraMapSubmonoid`	—	`Module.Finite.of_isLocalization` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `instIsScalarTowerLocalizationAlgebraMapSubmonoid` `Localization.isLocalization`
`instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors` 📖	mathematical	—	`Module.Finite` `FractionRing` `Localization` `CommRing.toCommMonoid` `Algebra.algebraMapSubmonoid` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `Algebra.toModule` `OreLocalization.instCommSemiring` `instAlgebraLocalizationAlgebraMapSubmonoid`	—	`IsScalarTower.right` `instIsScalarTowerLocalizationAlgebraMapSubmonoid` `Module.Finite.of_isLocalization` `OreLocalization.instIsScalarTower` `Localization.isLocalization`
`multiple_mem_adjoin_of_mem_localization_adjoin` 📖	mathematical	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin`	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Submonoid.instSetLike` `Submonoid.smul` `Algebra.toSMul`	—	`Algebra.adjoin_eq_span` `multiple_mem_span_of_mem_localization_span`
`multiple_mem_span_of_mem_localization_span` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.span`	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Submonoid.instSetLike` `Submonoid.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Submodule.mem_span_finite_of_mem_span` `Finset.induction_on` `Finset.coe_empty` `Submodule.span_empty` `one_smul` `Finset.coe_insert` `IsLocalization.surj` `Submodule.smul_mem` `smul_add` `smul_smul` `SubmonoidClass.toMulMemClass` `Submonoid.instSubmonoidClass` `mul_comm` `algebraMap_smul` `Algebra.smul_def` `smul_assoc` `Submodule.span_mono`

---

← Back to Index