Documentation Verification Report

FinitePresentation

📁 Source: Mathlib/RingTheory/FinitePresentation.lean

Statistics

Metric	Count
Definitions	0
Theorems `comp`, `comp_surjective`, `id`, `of_comp_finiteType`, `of_finiteType`, `of_surjective`, `of_finitePresentation`, `equiv`, `iff`, `iff_quotient_mvPolynomial'`, `ker_fG_of_surjective`, `ker_fg_of_mvPolynomial`, `mvPolynomial`, `mvPolynomial_of_finitePresentation`, `of_finiteType`, `of_restrict_scalars_finitePresentation`, `of_surjective`, `out`, `polynomial`, `quotient`, `self`, `trans`, `of_finitePresentation`, `comp`, `comp_surjective`, `id`, `of_bijective`, `of_comp_finiteType`, `of_finiteType`, `of_surjective`, `polynomial_induction`, `of_finitePresentation`, `finitePresentation_algebraMap`	33
Total	33

AlgHom.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`AlgHom.FinitePresentation` `AlgHom.comp` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHom.FinitePresentation.comp`
`comp_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike` `Ideal.FG` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `AlgHom.toRingHom`	`AlgHom.FinitePresentation` `AlgHom.comp`	—	`RingHom.instRingHomClass` `RingHom.FinitePresentation.comp_surjective`
`id` 📖	mathematical	—	`AlgHom.FinitePresentation` `AlgHom.id` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHom.FinitePresentation.id`
`of_comp_finiteType` 📖	mathematical	—	`AlgHom.FinitePresentation`	—	`RingHom.FinitePresentation.of_comp_finiteType`
`of_finiteType` 📖	mathematical	—	`AlgHom.FiniteType` `AlgHom.FinitePresentation`	—	`RingHom.FinitePresentation.of_finiteType`
`of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike` `Ideal.FG` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `AlgHom.toRingHom`	`AlgHom.FinitePresentation`	—	`RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHom.FinitePresentation.of_surjective`

AlgHom.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finitePresentation` 📖	mathematical	—	`AlgHom.FiniteType`	—	`RingHom.FiniteType.of_finitePresentation`

Algebra.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv` 📖	mathematical	—	`Algebra.FinitePresentation` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHom.instRingHomClass` `out` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgHom.coe_comp` `AlgEquiv.surjective` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingHom.ker_eq_comap_bot` `Ideal.comap_comap` `RingHom.ker_coe_equiv`
`iff` 📖	mathematical	—	`Algebra.FinitePresentation` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal.FG` `MvPolynomial` `MvPolynomial.commSemiring`	—	`RingHom.instRingHomClass` `equiv` `quotient` `Finite.of_fintype`
`iff_quotient_mvPolynomial'` 📖	mathematical	—	`Algebra.FinitePresentation` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial` `DFunLike.coe` `AlgHom` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `Ideal.FG` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `AlgHom.toRingHom`	—	`RingHom.instRingHomClass` `AlgEquiv.surjective` `Ideal.fg_ker_comp` `AlgHom.ker_coe_equiv` `Submodule.fg_bot` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`ker_fG_of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`Ideal.FG` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `AlgHom.toRingHom`	—	`RingHom.instRingHomClass` `out` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Ideal.comap_comap` `Ideal.map_comap_of_surjective` `Ideal.FG.map` `ker_fg_of_mvPolynomial`
`ker_fg_of_mvPolynomial` 📖	mathematical	`MvPolynomial` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike`	`Ideal.FG` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `AlgHom.toRingHom`	—	`RingHom.instRingHomClass` `out` `Finset.coe_union` `Finset.coe_image` `Finset.coe_univ` `Set.image_univ` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.coe_toRingHom` `MvPolynomial.map_aeval` `AlgHom.comp_algebraMap` `MvPolynomial.aeval_eq_eval₂Hom` `MvPolynomial.aeval_unique` `Ideal.span_le` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `sub_self` `Ideal.subset_span` `LE.le.antisymm` `MvPolynomial.adjoin_range_X` `Algebra.adjoin_induction` `sub_add_cancel` `add_comm` `AddSubmonoid.add_mem_sup` `Set.mem_range_self` `Submodule.subset_span` `Set.mem_union_left` `AddSubmonoid.mem_sup_left` `MvPolynomial.aeval_C` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddSubmonoid.instAddSubmonoidClass` `AddSubmonoid.mem_sup` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `add_assoc` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1` `Ideal.mul_mem_left` `Submodule.addSubmonoidClass` `Set.mem_union_right` `Set.mem_image_of_mem` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `add_zero`
`mvPolynomial` 📖	mathematical	—	`Algebra.FinitePresentation` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra`	—	`trans` `MvPolynomial.isScalarTower` `IsScalarTower.right`
`mvPolynomial_of_finitePresentation` 📖	mathematical	—	`Algebra.FinitePresentation` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra`	—	`RingHom.instRingHomClass` `iff_quotient_mvPolynomial'` `nonempty_fintype` `Finite.instSum` `Finite.of_fintype` `MvPolynomial.map_surjective` `AlgEquiv.surjective` `Ideal.fg_ker_comp` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.toAlgHom_eq_coe` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgEquiv.toAlgHom_toRingHom` `AlgHom.ker_coe_equiv` `Submodule.fg_bot` `AlgHom.toRingHom_eq_coe` `MvPolynomial.mapAlgHom_coe_ringHom` `MvPolynomial.ker_map` `Ideal.FG.map`
`of_finiteType` 📖	mathematical	—	`Algebra.FiniteType` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.FinitePresentation`	—	`Algebra.FiniteType.iff_quotient_mvPolynomial''` `RingHom.instRingHomClass` `IsNoetherian.noetherian` `MvPolynomial.isNoetherianRing` `Finite.of_fintype` `Algebra.FiniteType.of_finitePresentation`
`of_restrict_scalars_finitePresentation` 📖	mathematical	—	`Algebra.FinitePresentation` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHom.instRingHomClass` `out` `AlgHom.range_eq_top` `Algebra.adjoin_range_eq_range_aeval` `Set.range_comp` `Algebra.eq_top_iff` `Algebra.adjoin_adjoin_of_tower` `Algebra.adjoin_image` `MvPolynomial.adjoin_range_X` `Algebra.map_top` `Algebra.subset_adjoin` `Algebra.FiniteType.out` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Algebra.adjoin_union_eq_adjoin_adjoin` `Subalgebra.restrictScalars_top` `MvPolynomial.isScalarTower` `Algebra.adjoin_algebraMap` `Subalgebra.restrictScalars_injective` `Algebra.adjoin_restrictScalars` `Finset.coe_union` `Finset.coe_image` `Finset.attach_eq_univ` `Finset.coe_univ` `Set.image_univ` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Ideal.span_le` `SetLike.mem_coe` `RingHom.mem_ker` `MvPolynomial.aeval_map_algebraMap` `MvPolynomial.aeval_unique` `Ideal.subset_span` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `MvPolynomial.aeval_C` `sub_self` `LE.le.antisymm` `Algebra.adjoin_induction` `MvPolynomial.algebraMap_eq` `sub_add_cancel` `add_comm` `AddSubmonoid.add_mem_sup` `Set.mem_range_self` `Set.mem_union_right` `AddSubmonoid.mem_sup_left` `MvPolynomial.map_X` `MvPolynomial.map_C` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddSubmonoid.instAddSubmonoidClass` `AddSubmonoid.mem_sup` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `add_assoc` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Ideal.mul_mem_left` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1` `Set.mem_union_left` `Set.mem_image_of_mem` `Submodule.addSubmonoidClass` `add_zero` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass`
`of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike` `Ideal.FG` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `AlgHom.toRingHom`	`Algebra.FinitePresentation`	—	`RingHom.instRingHomClass` `equiv` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHom.instIsTwoSidedKer` `quotient`
`out` 📖	mathematical	—	`MvPolynomial` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `Ideal.FG` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `AlgHom.toRingHom`	—	—
`polynomial` 📖	mathematical	—	`Algebra.FinitePresentation` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra`	—	`equiv` `mvPolynomial` `self` `Finite.of_fintype` `trans` `Polynomial.isScalarTower` `IsScalarTower.right`
`quotient` 📖	mathematical	`Ideal.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Algebra.FinitePresentation` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient`	—	`RingHom.instRingHomClass` `out` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mkₐ_surjective` `Ideal.fg_ker_comp` `Ideal.Quotient.mkₐ_ker`
`self` 📖	mathematical	—	`Algebra.FinitePresentation` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`Finite.of_fintype` `equiv` `Empty.instIsEmpty`
`trans` 📖	mathematical	—	`Algebra.FinitePresentation` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`iff` `equiv` `quotient` `mvPolynomial_of_finitePresentation` `Finite.of_fintype` `Ideal.Quotient.isScalarTower` `MvPolynomial.isScalarTower` `IsScalarTower.right`

Algebra.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finitePresentation` 📖	mathematical	—	`Algebra.FiniteType` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHom.instRingHomClass` `Algebra.FinitePresentation.out` `iff_quotient_mvPolynomial''`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finitePresentation_algebraMap` 📖	mathematical	—	`FinitePresentation` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.FinitePresentation`	—	`FinitePresentation.eq_1` `toAlgebra_algebraMap`

RingHom.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`RingHom.FinitePresentation` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsScalarTower.of_algebraMap_eq'` `Algebra.FinitePresentation.trans`
`comp_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ideal.FG` `RingHom.ker` `RingHom.instRingHomClass`	`RingHom.FinitePresentation` `RingHom.comp`	—	`RingHom.instRingHomClass` `Algebra.FinitePresentation.of_surjective` `OneHom.map_one'` `MonoidHom.map_mul'` `RingHom.map_zero'` `RingHom.map_add'`
`id` 📖	mathematical	—	`RingHom.FinitePresentation` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Algebra.FinitePresentation.self`
`of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`RingHom.FinitePresentation`	—	`of_surjective` `RingHom.instRingHomClass` `RingHom.injective_iff_ker_eq_bot` `Submodule.fg_bot`
`of_comp_finiteType` 📖	mathematical	—	`RingHom.FinitePresentation`	—	`IsScalarTower.of_algebraMap_eq'` `Algebra.FinitePresentation.of_restrict_scalars_finitePresentation`
`of_finiteType` 📖	mathematical	—	`RingHom.FiniteType` `RingHom.FinitePresentation`	—	`Algebra.FinitePresentation.of_finiteType`
`of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ideal.FG` `RingHom.ker` `RingHom.instRingHomClass`	`RingHom.FinitePresentation`	—	`RingHom.instRingHomClass` `RingHom.comp_id` `comp_surjective` `id`
`polynomial_induction` 📖	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.commRing` `Polynomial.C` `RingHom.comp` `Semiring.toNonAssocSemiring`	—	—	`RingHom.instRingHomClass` `AlgHom.comp_algebraMap` `MvPolynomial.C_surjective` `Fin.isEmpty'` `RingHom.comap_ker` `Ideal.comap_symm` `Ideal.FG.map` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.surjective` `RingHom.comp_assoc` `RingHom.ext` `MvPolynomial.ext` `MvPolynomial.coeff_C` `MvPolynomial.aevalTower_C` `Polynomial.aeval_C` `MvPolynomial.algHom_C`

RingHom.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finitePresentation` 📖	mathematical	—	`RingHom.FiniteType`	—	`Algebra.FiniteType.of_finitePresentation`

---

← Back to Index