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 CommSemiring.toSemiring adjoin 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	—	Subalgebra.setRange_algebraMap map_top Subalgebra.ext IsScalarTower.subalgebra' IsScalarTower.right
fg_trans' 📖	mathematical	Subalgebra.FG CommSemiring.toSemiring Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Subalgebra.FG 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	Subalgebra CommSemiring.toSemiring Subalgebra.FG Submodule.FG SetLike.instMembership Subalgebra.instSetLike Subalgebra.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra.moduleLeft Algebra.toModule Top.top Submodule Submodule.instTop	—	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 📖	mathematical	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	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	—	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 RingHomInvPair.ids IsScalarTower.subalgebra

---

← Back to Index