Documentation Verification Report

ReesAlgebra

📁 Source: Mathlib/RingTheory/ReesAlgebra.lean

Statistics

Metric	Count
Definitions `reesAlgebra`	1
Theorems `adjoin_monomial_eq_reesAlgebra`, `instFiniteTypeSubtypePolynomialMemSubalgebraReesAlgebraOfIsNoetherianRing`, `instIsNoetherianRingSubtypePolynomialMemSubalgebraReesAlgebra`, `mem_reesAlgebra_iff`, `mem_reesAlgebra_iff_support`, `monomial_mem_adjoin_monomial`, `fg`, `monomial_mem`	8
Total	9

(root)

Definitions

Name	Category	Theorems
`reesAlgebra` 📖	CompOp	13 math math: `Ideal.Filtration.submodule_closure_single`, `Ideal.Filtration.submodule_eq_span_le_iff_stable_ge`, `mem_reesAlgebra_iff_support`, `Ideal.Filtration.mem_submodule`, `adjoin_monomial_eq_reesAlgebra`, `instIsNoetherianRingSubtypePolynomialMemSubalgebraReesAlgebra`, `reesAlgebra.monomial_mem`, `Ideal.Filtration.inf_submodule`, `Ideal.Filtration.submodule_span_single`, `reesAlgebra.fg`, `mem_reesAlgebra_iff`, `instFiniteTypeSubtypePolynomialMemSubalgebraReesAlgebraOfIsNoetherianRing`, `Ideal.Filtration.submodule_fg_iff_stable`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_monomial_eq_reesAlgebra` 📖	mathematical	—	`Algebra.adjoin` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `SetLike.coe` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `Submodule.setLike` `Submodule.map` `RingHom.id` `RingHomSurjective.ids` `Polynomial.monomial` `reesAlgebra`	—	`le_antisymm` `RingHomSurjective.ids` `Algebra.adjoin_le` `IsScalarTower.right` `reesAlgebra.monomial_mem` `pow_one` `Polynomial.as_sum_support` `Subalgebra.sum_mem` `monomial_mem_adjoin_monomial`
`instFiniteTypeSubtypePolynomialMemSubalgebraReesAlgebraOfIsNoetherianRing` 📖	mathematical	—	`Algebra.FiniteType` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subalgebra` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `reesAlgebra` `Subalgebra.toSemiring` `Subalgebra.algebra`	—	`Subalgebra.fg_top` `reesAlgebra.fg` `IsNoetherian.noetherian`
`instIsNoetherianRingSubtypePolynomialMemSubalgebraReesAlgebra` 📖	mathematical	—	`IsNoetherianRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subalgebra` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `reesAlgebra` `Subalgebra.toSemiring`	—	`Algebra.FiniteType.isNoetherianRing` `instFiniteTypeSubtypePolynomialMemSubalgebraReesAlgebraOfIsNoetherianRing`
`mem_reesAlgebra_iff` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subalgebra` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `reesAlgebra` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Polynomial.coeff`	—	—
`mem_reesAlgebra_iff_support` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subalgebra` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `reesAlgebra` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Polynomial.coeff`	—	`IsScalarTower.right` `Polynomial.mem_support_iff` `imp_iff_not_or` `Ideal.zero_mem`
`monomial_mem_adjoin_monomial` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	`Polynomial` `Subalgebra` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Subalgebra.instSetLike` `Algebra.adjoin` `SetLike.coe` `Submodule` `Polynomial.module` `Submodule.map` `RingHom.id` `RingHomSurjective.ids` `Polynomial.monomial` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`IsScalarTower.right` `RingHomSurjective.ids` `Subalgebra.algebraMap_mem` `Submodule.smul_induction_on` `pow_succ'` `add_comm` `smul_eq_mul` `Polynomial.monomial_mul_monomial` `Subalgebra.mul_mem` `Algebra.subset_adjoin` `Set.mem_image_of_mem` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `Subalgebra.add_mem`

reesAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg` 📖	mathematical	`Ideal.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Subalgebra.FG` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `reesAlgebra`	—	`RingHomSurjective.ids` `adjoin_monomial_eq_reesAlgebra` `Finset.coe_image` `Submodule.map_span` `Algebra.adjoin_span`
`monomial_mem` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subalgebra` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `reesAlgebra` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.monomial` `Ideal` `Submodule.setLike` `Submodule.instPowNat` `IsScalarTower.right`	—	`IsScalarTower.right` `Polynomial.coeff_monomial` `Polynomial.coeff_monomial_same` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`

---

← Back to Index