Documentation Verification Report

Finite

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

Statistics

Metric	Count
Definitions `Finite`	1
Theorems `finite_containsIdentities`, `finite_isStableUnderBaseChange`, `finite_localizationPreserves`, `finite_ofLocalizationSpan`, `finite_respectsIso`, `finite_stableUnderComposition`, `localization_away_map_finite`	7
Total	8

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`

---

← Back to Index