Tower

📁 Source: Mathlib/RingTheory/Adjoin/Tower.lean

Statistics

Metric	Count
Definitions	0
Theorems adjoin_res_eq_adjoin_res, adjoin_restrictScalars, fg_trans', exists_subalgebra_of_fg, fg_of_fg_of_fg	5
Total	5

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_res_eq_adjoin_res 📖	mathematical	adjoin CommSemiring.toSemiring Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Subalgebra.restrictScalars Set.image DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	IsScalarTower.subalgebra' IsScalarTower.right adjoin_restrictScalars adjoin_image AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.coe_toRingHom IsScalarTower.coe_toAlgHom adjoin_union_eq_adjoin_adjoin Set.union_comm
adjoin_restrictScalars 📖	mathematical	—	Subalgebra.restrictScalars CommSemiring.toSemiring adjoin Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.map IsScalarTower.toAlgHom Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Subalgebra.toCommSemiring Subalgebra.algebra Subalgebra.toAlgebra id IsScalarTower.subalgebra' IsScalarTower.right	—	Set.ext mem_top Subalgebra.ext IsScalarTower.subalgebra' IsScalarTower.right
fg_trans' 📖	—	Subalgebra.FG CommSemiring.toSemiring Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—	Finset.coe_union Finset.coe_image IsScalarTower.subalgebra' adjoin_algebraMap_image_union_eq_adjoin_adjoin IsScalarTower.subalgebra adjoin_top Subalgebra.restrictScalars_top

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_subalgebra_of_fg 📖	mathematical	Subalgebra.FG Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Submodule.FG CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Submodule Submodule.instTop	SetLike.instMembership Subalgebra.instSetLike Subalgebra.toSemiring Subalgebra.moduleLeft	—	sum_mem Submodule.addSubmonoidClass Submodule.smul_mem Algebra.subset_adjoin Finset.mem_image₂_of_mem Finset.mem_union_left Submodule.subset_span Finset.mem_insert_of_mem IsScalarTower.right Submodule.span_mul_span Submodule.span_le Finset.coe_insert mul_one Set.mem_insert one_mul Set.mem_insert_of_mem SetLike.mem_coe Finset.mem_union_right Finset.mul_mem_mul Subalgebra.fg_adjoin_finset Submodule.restrictScalars_injective IsScalarTower.subalgebra' Submodule.restrictScalars_top eq_top_iff Algebra.top_toSubmodule Algebra.adjoin_eq_span Submonoid.closure_induction Finset.mem_insert_self Submodule.mul_mem_mul
fg_of_fg_of_fg 📖	—	Subalgebra.FG CommRing.toCommSemiring CommSemiring.toSemiring Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Submodule.FG NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Submodule Submodule.instTop DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	—	exists_subalgebra_of_fg Algebra.fg_trans' IsScalarTower.subalgebra' IsScalarTower.right Subalgebra.fg_top Subalgebra.fg_of_submodule_fg isNoetherianRing_of_fg fg_of_injective isNoetherian_of_isNoetherianRing_of_finite IsScalarTower.subalgebra

---

← Back to Index