Documentation Verification Report

FinitePresentation

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

Statistics

Metric	Count
Definitions `FinitePresentation`, `FinitePresentation`	2
Theorems `finitePresentation_holdsForLocalizationAway`, `finitePresentation_isLocal`, `finitePresentation_isStableUnderBaseChange`, `finitePresentation_localizationPreserves`, `finitePresentation_ofLocalizationSpanTarget`, `finitePresentation_respectsIso`, `finitePresentation_stableUnderComposition`	7
Total	9

AlgHom

Definitions

Name	Category	Theorems
`FinitePresentation` 📖	MathDef	7 math math: `MvPolynomial.finitePresentation_universalFactorizationMap`, `FinitePresentation.of_comp_finiteType`, `FinitePresentation.id`, `FinitePresentation.of_finiteType`, `FinitePresentation.of_surjective`, `FinitePresentation.comp`, `FinitePresentation.comp_surjective`

RingHom

Definitions

Name	Category	Theorems
`FinitePresentation` 📖	MathDef	24 math math: `finitePresentation_stableUnderComposition`, `Smooth.finitePresentation`, `Etale.iff_flat_and_formallyUnramified`, `finitePresentation_respectsIso`, `FinitePresentation.of_finiteType`, `AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE`, `FinitePresentation.comp_surjective`, `finitePresentation_isLocal`, `FinitePresentation.of_comp_finiteType`, `AlgebraicGeometry.instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation`, `finitePresentation_localizationPreserves`, `AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE`, `finitePresentation_algebraMap`, `FinitePresentation.comp`, `FinitePresentation.of_bijective`, `AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_of_affine_subset`, `finitePresentation_isStableUnderBaseChange`, `AlgebraicGeometry.locallyOfFinitePresentation_iff`, `FinitePresentation.codescendsAlong_faithfullyFlat`, `FinitePresentation.of_surjective`, `FinitePresentation.id`, `finitePresentation_ofLocalizationSpanTarget`, `smooth_def`, `finitePresentation_holdsForLocalizationAway`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finitePresentation_holdsForLocalizationAway` 📖	mathematical	—	`HoldsForLocalizationAway` `FinitePresentation`	—	`finitePresentation_algebraMap` `IsLocalization.Away.finitePresentation`
`finitePresentation_isLocal` 📖	mathematical	—	`PropertyIsLocal` `FinitePresentation`	—	`LocalizationPreserves.away` `finitePresentation_localizationPreserves` `finitePresentation_ofLocalizationSpanTarget` `OfLocalizationSpanTarget.ofLocalizationSpan` `StableUnderComposition.stableUnderCompositionWithLocalizationAway` `finitePresentation_stableUnderComposition` `finitePresentation_holdsForLocalizationAway`
`finitePresentation_isStableUnderBaseChange` 📖	mathematical	—	`IsStableUnderBaseChange` `FinitePresentation`	—	`finitePresentation_respectsIso` `Algebra.to_smulCommClass` `Algebra.FinitePresentation.baseChange`
`finitePresentation_localizationPreserves` 📖	mathematical	—	`LocalizationPreserves` `FinitePresentation`	—	`IsStableUnderBaseChange.localizationPreserves` `finitePresentation_isStableUnderBaseChange`
`finitePresentation_ofLocalizationSpanTarget` 📖	mathematical	—	`OfLocalizationSpanTarget` `FinitePresentation`	—	`IsScalarTower.Algebra.ext` `Algebra.smul_def` `Algebra.FinitePresentation.of_span_eq_top_target`
`finitePresentation_respectsIso` 📖	mathematical	—	`RespectsIso` `FinitePresentation`	—	`StableUnderComposition.respectsIso` `finitePresentation_stableUnderComposition` `FinitePresentation.of_surjective` `RingEquiv.surjective` `instRingHomClass` `ker_coe_equiv` `Submodule.fg_bot`
`finitePresentation_stableUnderComposition` 📖	mathematical	—	`StableUnderComposition` `FinitePresentation`	—	`FinitePresentation.comp`

---

← Back to Index