Basic

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

Statistics

Metric	Count
Definitions	0
Theorems restrictScalars_adjoin, adjoin_adjoin_of_tower, adjoin_algebraMap, adjoin_algebraMap_image_union_eq_adjoin_adjoin, adjoin_eq_adjoin_union, adjoin_inl_union_inr_eq_prod, adjoin_nonUnitalSubalgebra_eq_span, adjoin_prod_le, adjoin_top, adjoin_union_eq_adjoin_adjoin, pow_smul_mem_adjoin_smul, pow_smul_mem_of_smul_subset_of_mem_adjoin, restrictScalars_adjoin, restrictScalars_adjoin_of_algEquiv, adjoin_eq_span_basis	15
Total	15

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_adjoin_of_tower 📖	mathematical	—	adjoin SetLike.coe Subalgebra Subalgebra.instSetLike	—	le_antisymm adjoin_le Subalgebra.coe_restrictScalars SetLike.coe_subset_coe instIsConcreteLE subset_adjoin adjoin_mono
adjoin_algebraMap 📖	mathematical	—	adjoin Set.image DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Subalgebra.map IsScalarTower.toAlgHom	—	adjoin_image
adjoin_algebraMap_image_union_eq_adjoin_adjoin 📖	mathematical	—	adjoin Set Set.instUnion Set.image DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Subalgebra.restrictScalars Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommSemiring Subalgebra.algebra Subalgebra.toAlgebra IsScalarTower.subalgebra'	—	le_antisymm IsScalarTower.subalgebra' Subsemiring.closure_mono Set.union_subset Set.range_subset_iff IsScalarTower.algebraMap_apply Set.union_subset_union_left subset_adjoin Subsemiring.closure_le adjoin_mono Set.subset_union_left Subtype.prop adjoin_algebraMap Set.Subset.trans Set.subset_union_right
adjoin_eq_adjoin_union 📖	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 Set.instUnion Set.image DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	IsScalarTower.subalgebra' IsScalarTower.right adjoin_union_eq_adjoin_adjoin IsScalarTower.coe_toAlgHom' AlgHom.map_adjoin map_top IsScalarTower.adjoin_range_toAlgHom
adjoin_inl_union_inr_eq_prod 📖	mathematical	—	adjoin Prod.instSemiring Prod.algebra Set Set.instUnion Set.image DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAddCommMonoid toModule Prod.instModule LinearMap.instFunLike LinearMap.inl Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne LinearMap.inr Subalgebra.prod	—	le_antisymm Set.image_congr Set.union_singleton Set.mk_preimage_prod_left Set.mk_preimage_prod_right mem_adjoin_of_map_mul LinearMap.inl_map_mul LinearMap.inr_map_mul adjoin_mono Set.subset_union_left Set.subset_union_right add_zero zero_add Subalgebra.add_mem
adjoin_nonUnitalSubalgebra_eq_span 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra CommSemiring.toSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule adjoin SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Submodule.span Set Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne NonUnitalSubalgebra.toSubmodule	—	adjoin_eq_span Submonoid.closure_eq_one_union Submodule.span_union IsScalarTower.right to_smulCommClass NonUnitalAlgebra.adjoin_eq_span NonUnitalAlgebra.adjoin_eq
adjoin_prod_le 📖	mathematical	—	Subalgebra Prod.instSemiring Prod.algebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder adjoin SProd.sprod Set Set.instSProd Subalgebra.prod	—	adjoin_le Set.prod_mono subset_adjoin
adjoin_top 📖	mathematical	—	adjoin Subalgebra CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Subalgebra.toCommSemiring Subalgebra.toAlgebra Subalgebra.restrictScalars id IsScalarTower.subalgebra	—	Subalgebra.algebraMap_mem IsScalarTower.subalgebra SetLike.coe_injective le_antisymm adjoin_le subset_adjoin OrderIso.symm_apply_le
adjoin_union_eq_adjoin_adjoin 📖	mathematical	—	adjoin CommSemiring.toSemiring Set Set.instUnion Subalgebra.restrictScalars Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommSemiring Subalgebra.algebra Subalgebra.toAlgebra id IsScalarTower.subalgebra' IsScalarTower.right	—	IsScalarTower.subalgebra' IsScalarTower.right Set.image_congr Set.image_id' adjoin_algebraMap_image_union_eq_adjoin_adjoin
pow_smul_mem_adjoin_smul 📖	mathematical	Subalgebra CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike adjoin	Set Set.smulSet toSMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	pow_smul_mem_of_smul_subset_of_mem_adjoin IsScalarTower.left subset_adjoin Subalgebra.algebraMap_mem
pow_smul_mem_of_smul_subset_of_mem_adjoin 📖	mathematical	Set Set.instHasSubset Set.smulSet toSMul CommSemiring.toSemiring SetLike.coe Subalgebra Subalgebra.instSetLike SetLike.instMembership adjoin DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Finsupp.mem_span_iff_linearCombination adjoin_eq_span Finsupp.smul_sum Submodule.sum_mem le_trans Finset.le_sup tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub pow_add smul_smul IsScalarTower.algebraMap_smul mul_comm smul_def map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Subalgebra.mul_mem Subalgebra.pow_mem Subalgebra.smul_mem Submonoid.closure_eq Submonoid.closure_mono Submonoid.pow_smul_mem_closure_smul IsScalarTower.right Subtype.prop
restrictScalars_adjoin 📖	mathematical	—	Subalgebra.restrictScalars Subalgebra CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommSemiring Subalgebra.algebra Subalgebra.toAlgebra id IsScalarTower.subalgebra' IsScalarTower.right adjoin Set Set.instUnion SetLike.coe	—	IsScalarTower.subalgebra' IsScalarTower.right adjoin_eq adjoin_union_eq_adjoin_adjoin
restrictScalars_adjoin_of_algEquiv 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap AlgEquiv AlgEquiv.instFunLike	Subalgebra.restrictScalars adjoin	—	SetLike.ext'_iff Set.range_comp EquivLike.range_eq_univ Set.image_univ

Algebra.Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictScalars_adjoin 📖	mathematical	—	Subalgebra.restrictScalars Algebra.adjoin Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra AlgHom.range CommSemiring.toSemiring IsScalarTower.toAlgHom	—	le_antisymm Algebra.adjoin_induction le_sup_right Algebra.subset_adjoin le_sup_left AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass Subalgebra.mem_restrictScalars sup_le algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSMulMemClass Algebra.adjoin_le

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_eq_span_basis 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding toSubmodule Algebra.adjoin SetLike.coe instSetLike Submodule.span Set.range SetLike.instMembership Module.Basis toSemiring instModuleSubtypeMem Module.Basis.instFunLike	—	adjoin_eq_span_of_eq_span range_val RingHomSurjective.ids NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Submodule.map_top Submodule.map_span Module.Basis.span_eq

---

← Back to Index