Lattice

📁 Source: Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

Statistics

Metric	Count
Definitions adjoin, adjoinCommRingOfComm, adjoinCommSemiringOfComm, botEquiv, botEquivOfInjective, delabAdjoinNotation, gi, instCompleteLatticeSubalgebra, instInhabitedSubalgebra, instSubtypeMemSubalgebraMin, instSubtypeMemSubalgebraMin_1, subalgebra_adjoin, toTop, instUnique, saturation, toNonUnitalSubalgebraOrderEmbedding, topEquiv, closureEquivAdjoinInt, closureEquivAdjoinNat	19
Theorems subsingleton_left, subsingleton_right, adjoin_ext, adjoin_le_equalizer, eqOn_adjoin_iff, eqOn_sup, equalizer_eq_top, equalizer_same, ext_of_adjoin_eq_top, ext_of_eq_adjoin, ext_on_codisjoint, map_adjoin, map_adjoin_singleton, range_eq_top, subsingleton, adjoin_adjoin_coe_preimage, adjoin_attach_biUnion, adjoin_empty, adjoin_eq, adjoin_eq_of_le, adjoin_eq_ring_closure, adjoin_eq_sInf, adjoin_eq_span, adjoin_eq_span_of_subset, adjoin_iUnion, adjoin_image, adjoin_induction, adjoin_induction₂, adjoin_insert_adjoin, adjoin_insert_algebraMap, adjoin_insert_intCast, adjoin_insert_natCast, adjoin_insert_one, adjoin_insert_zero, adjoin_int, adjoin_le, adjoin_le_centralizer_centralizer, adjoin_le_iff, adjoin_mono, adjoin_nat, adjoin_nonUnitalSubalgebra, adjoin_singleton_algebraMap, adjoin_singleton_intCast, adjoin_singleton_le, adjoin_singleton_natCast, adjoin_singleton_one, adjoin_singleton_zero, adjoin_span, adjoin_toSubmodule_le, adjoin_toSubsemiring, adjoin_union, adjoin_union_coe_submodule, adjoin_univ, bijective_algebraMap_iff, botEquiv_symm_apply, coe_bot, coe_iInf, coe_inf, coe_sInf, coe_top, comap_top, commute_of_mem_adjoin_of_forall_mem_commute, commute_of_mem_adjoin_self, commute_of_mem_adjoin_singleton_of_commute, eq_top_iff, forall_mem_adjoin_smul_eq_self_iff, gc, iInf_toSubmodule, iInf_toSubsemiring, iSup_induction, iSup_induction', iSup_toSubsemiring, inf_toSubmodule, inf_toSubsemiring, instIsMulCommutative_adjoin, isMulCommutative_adjoin, isMulCommutative_adjoin_singleton, map_bot, map_iInf, map_inf, map_sup, map_top, mem_adjoin_iff, mem_adjoin_of_map_mul, mem_adjoin_of_mem, mem_bot, mem_iInf, mem_iSup_of_mem, mem_inf, mem_sInf, mem_sup_left, mem_sup_right, mem_top, mul_mem_sup, range_id, range_ofId, sInf_toSubmodule, sInf_toSubsemiring, sSup_def, sSup_toSubsemiring, self_mem_adjoin_singleton, span_le_adjoin, subset_adjoin, sup_def, sup_toSubsemiring, surjective_algebraMap_iff, toSubmodule_bot, toSubmodule_eq_top, toSubring_bot, toSubring_eq_top, toSubsemiring_eq_top, top_toSubmodule, top_toSubring, top_toSubsemiring, adjoin_le_algebra_adjoin, adjoin_eq_span_of_eq_span, center_eq_top, centralizer_eq_top_iff_subset, comap_map_eq, comap_map_eq_self, le_saturation, map_comap_eq, map_comap_eq_self, map_comap_eq_self_of_surjective, mem_saturation_iff, mem_saturation_of_mul_mem_left, mem_saturation_of_mul_mem_right, saturation_saturation, toNonUnitalSubalgebra_le_toNonUnitalSubalgebra, toNonUnitalSubalgebra_mono, topEquiv_apply, topEquiv_symm_apply_coe, adjoin_eq_span_of_eq_span	133
Total	152

AlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subsingleton_left 📖	mathematical	—	AlgEquiv	—	ext AlgHom.ext_iff AlgHom.subsingleton
subsingleton_right 📖	mathematical	—	AlgEquiv	—	symm_symm subsingleton_left

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_ext 📖	—	DFunLike.coe AlgHom Subalgebra SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Subalgebra.toSemiring Subalgebra.algebra funLike Algebra.subset_adjoin	—	—	Algebra.subset_adjoin ext Algebra.adjoin_induction algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass Subalgebra.instSMulMemClass commutes AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass instNonUnitalAlgHomClassOfAlgHomClass algHomClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass
adjoin_le_equalizer 📖	mathematical	Set.EqOn DFunLike.coe AlgHom funLike	Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Algebra.adjoin equalizer AlgHom funLike algHomClass	—	Algebra.adjoin_le algHomClass
eqOn_adjoin_iff 📖	mathematical	—	Set.EqOn DFunLike.coe AlgHom funLike SetLike.coe Subalgebra Subalgebra.instSetLike Algebra.adjoin	—	algHomClass instIsConcreteLE
eqOn_sup 📖	mathematical	Set.EqOn DFunLike.coe SetLike.coe Subalgebra Subalgebra.instSetLike	Set.EqOn DFunLike.coe SetLike.coe Subalgebra Subalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra	—	le_equalizer sup_le
equalizer_eq_top 📖	mathematical	—	equalizer Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
equalizer_same 📖	mathematical	—	equalizer Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	equalizer_eq_top
ext_of_adjoin_eq_top 📖	—	Algebra.adjoin Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.EqOn DFunLike.coe AlgHom funLike	—	—	ext adjoin_le_equalizer
ext_of_eq_adjoin 📖	—	Algebra.adjoin DFunLike.coe AlgHom Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.toSemiring Subalgebra.algebra funLike Eq.ge PartialOrder.toPreorder Subalgebra.instPartialOrder Algebra.subset_adjoin	—	—	Eq.ge Algebra.subset_adjoin adjoin_ext
ext_on_codisjoint 📖	—	Codisjoint Subalgebra Subalgebra.instPartialOrder BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Algebra.instCompleteLatticeSubalgebra Set.EqOn DFunLike.coe SetLike.coe Subalgebra.instSetLike	—	—	DFunLike.ext eqOn_sup Codisjoint.eq_top
map_adjoin 📖	mathematical	—	Subalgebra.map Algebra.adjoin Set.image DFunLike.coe AlgHom funLike	—	Algebra.adjoin_image
map_adjoin_singleton 📖	mathematical	—	Subalgebra.map Algebra.adjoin Set Set.instSingletonSet DFunLike.coe AlgHom funLike	—	map_adjoin Set.image_singleton
range_eq_top 📖	mathematical	—	range Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe AlgHom funLike	—	Algebra.eq_top_iff
subsingleton 📖	mathematical	—	AlgHom	—	ext Algebra.mem_top Set.mem_range Algebra.mem_bot commutes

Algebra

Definitions

Name	Category	Theorems
adjoin 📖	CompOp	327 math math: IsAlgebraic.adjoin_singleton, IsCyclotomicExtension.adjoin_primitive_root_eq_top, IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, minpoly.ToAdjoin.injective, NonUnitalAlgebra.adjoin_le_algebra_adjoin, RingHom.adjoin_algebraMap_apply, lift_cardinalMk_adjoin_le, IntermediateField.adjoin_eq_top_iff_of_isAlgebraic, polynomialFunctions.eq_adjoin_X, Subalgebra.adjoin_rank_le, AlgebraicIndependent.transcendental_adjoin_iff, AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm, FiniteType.adjoin_of_finite, algebraicIndependent_adjoin, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow, IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic, adjoin_algebraMap_image_union_eq_adjoin_adjoin, adjoin_singleton_intCast, AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic, jacobiSum_mem_algebraAdjoin_of_pow_eq_one, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero, MvPolynomial.aeval_range, finite_adjoin_simple_of_isIntegral, MulChar.apply_mem_algebraAdjoin_of_pow_eq_one, Subalgebra.comap_map_eq, Subalgebra.finrank_sup_eq_finrank_right_mul_finrank_of_free, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, TensorAlgebra.adjoin_range_ι, DualNumber.range_lift, AlgebraicIndependent.transcendental_adjoin, Subalgebra.star_adjoin_comm, IsIntegral.adjoin, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, adjoin_le_integralClosure, sSup_def, AlgebraicIndependent.repr_ker, isAlgebraic_adjoin_iff, CliffordAlgebra.range_lift, IsLocalization.lift_mem_adjoin_finsetIntegerMultiple, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, adjoin_singleton_algebraMap, NumberField.adjoin_eq_top_of_infinitePlace_lt, Subalgebra.rank_sup_eq_rank_left_mul_rank_of_free, AlgebraicIndependent.iff_adjoin_image_compl, MulChar.apply_mem_algebraAdjoin, adjoin_insert_natCast, RingHom.adjoinAlgebraMap_surjective, Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left, Polynomial.lift_of_splits, mem_adjoin_iff, MvPolynomial.supported_eq_adjoin_X, MonoidAlgebra.mem_adjoin_support, IntermediateField.algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin, Submonoid.adjoin_eq_span_of_eq_span, adjoin_monomial_eq_reesAlgebra, IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic, AlgebraicIndependent.matroid_isBasis_iff, HomogeneousLocalization.Away.adjoin_mk_prod_pow_eq_top, EssFiniteType.adjoin_mem_finset, IsScalarTower.adjoin_range_toAlgHom, adjoin_attach_biUnion, Polynomial.IsSplittingField.adjoin_rootSet, adjoin_span, IntermediateField.isAlgebraic_adjoin_iff_top, AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, MonoidAlgebra.support_gen_of_gen', AdjoinRoot.Minpoly.toAdjoin.surjective, AlgebraicIndependent.aeval_comp_repr, span_le_adjoin, adjoin_adjoin_of_tower, AlgebraicIndependent.adjoin_iff_disjoint, IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_one, adjoin_union, IntermediateField.isAlgebraic_adjoin_iff, AlgebraicIndependent.matroid_spanning_iff, Polynomial.SplittingFieldAux.adjoin_rootSet, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, prod_mem_ideal_map_of_mem_conductor, mem_adjoin_map_integralClosure_of_isStandardEtale, adjoin_singleton_zero, NonUnitalSubalgebra.unitization_range, IsPrimitiveRoot.adjoin_pair_eq, monomial_mem_adjoin_monomial, subset_adjoin, Subalgebra.op_adjoin, MvPolynomial.adjoin_range_X, isAlgebraic_adjoin_singleton_iff, adjoin_eq_top_of_conductor_eq_top, Polynomial.algEquivOfTranscendental_coe, adjoin_insert_one, AlgebraicIndependent.sumElim_iff, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime, span_coeff_minpolyDiv, multiple_mem_adjoin_of_mem_localization_adjoin, IntermediateField.adjoin_simple_toSubalgebra_of_integral, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, Subalgebra.fg_adjoin_finset, isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, Polynomial.adjoin_rootSet_eq_range, AlgebraicIndependent.adjoin_of_disjoint, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', essFiniteType_cond_iff, CliffordAlgebra.adjoin_range_ι, instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap, Polynomial.Splits.adjoin_rootSet_eq_range, adjoin.powerBasis_dim, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous, adjoin_eq_ring_closure, adjoin_singleton_le, AdjoinRoot.Minpoly.coe_toAdjoin, mem_conductor_iff, traceForm_dualSubmodule_adjoin, FractionalIdeal.adjoinIntegral_coe, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, adjoin_nonUnitalSubalgebra_eq_span, adjoin_insert_algebraMap, isNoetherian_adjoin_finset, adjoin_singleton_eq_range_aeval, Transcendental.uniqueFactorizationMonoid_adjoin, IntermediateField.adjoin_simple_eq_top_iff_of_isAlgebraic, isCyclotomicExtension_iff_eq_adjoin, FractionalIdeal.isFractional_adjoin_integral, Subalgebra.fg_def, PowerBasis.adjoin_gen_eq_top, adjoin_range_eq_range_freeAlgebra_lift, coeff_minpolyDiv_mem_adjoin, Polynomial.algEquivOfTranscendental_symm_gen, Complex.range_liftAux, Subalgebra.adjoin_eq_span_basis, adjoin.powerBasis'_dim, fg_trans, AlgebraicIndependent.isAlgebraic_adjoin_iff_of_matroid_isBasis, IntermediateField.mem_adjoin_iff_div, isMulCommutative_adjoin_singleton, ContinuousAlgHom.eqOn_closure_adjoin, conductor_subset_adjoin, exists_jacobiSum_eq_neg_one_add, Derivation.eqOn_adjoin, adjoin_toSubmodule_le, adjoin_eq_top_of_primitive_element, Presentation.instHasCoeffsSubtypeMemSubalgebraAdjoin, NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, MonoidAlgebra.exists_finset_adjoin_eq_top, quotAdjoinEquivQuotMap_apply_mk, PowerBasis.adjoin_eq_top_of_gen_mem_adjoin, Polynomial.IsSplittingField.adjoin_rootSet', AlgHom.map_adjoin, Polynomial.algEquivOfTranscendental_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, adjoin.powerBasis_gen, Unitization.lift_range, AlgebraicIndependent.option_iff_transcendental, adjoin_singleton_one, adjoin_eq_span_of_subset, discr_mul_isIntegral_mem_adjoin, isMulCommutative_adjoin, IntermediateField.adjoin_eq_algebra_adjoin, AlgebraicIndependent.algebraMap_aevalEquiv, AdjoinRoot.Minpoly.coe_toAdjoin_mk_X, IsCyclotomicExtension.iff_singleton, adjoin_range_eq_range_aeval, MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero, IsAlgebraic.adjoin_of_forall_isAlgebraic, adjoin_inl_union_inr_eq_prod, finite_adjoin_of_finite_of_isIntegral, adjoin_insert_intCast, Subalgebra.finrank_sup_eq_finrank_left_mul_finrank_of_free, Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree, adjoin_insert_adjoin, IntermediateField.isTranscendenceBasis_adjoin_iff, IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left, small_adjoin, Submodule.span_range_natDegree_eq_adjoin, adjoin_eq_exists_aeval, adjoin_nonUnitalSubalgebra, AlgebraicIndepOn.insert_iff, RatFunc.irreducible_minpolyX', IntermediateField.algebraAdjoinAdjoin.algebraMap_eq_gen_self, adjoin_singleton_natCast, Subalgebra.unop_adjoin, AddMonoidAlgebra.exists_finset_adjoin_eq_top, adjoin_image, Subalgebra.rank_sup_eq_rank_right_mul_rank_of_free, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic, Module.End.exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow, FreeAlgebra.adjoin_range_ι, adjoin_eq_adjoin_union, isAlgebraic_iff_exists_isTranscendenceBasis_subset, adjoin_union_coe_submodule, isCyclotomicExtension_singleton_iff_eq_adjoin, AlgebraicIndependent.aeval_repr, MonoidAlgebra.support_gen_of_gen, AlgHom.eqOn_adjoin_iff, adjoin_adjoin_coe_preimage, fg_adjoin_of_finite, adjoin_top, pow_smul_mem_adjoin_smul, adjoin_le_centralizer_centralizer, adjoin_root_eq_top_of_isSplittingField, mem_adjoin_of_mem, adjoin_eq_range, adjoin_eq_span, TensorAlgebra.range_lift, IntermediateField.adjoin_toSubalgebra, DualNumber.range_inlAlgHom_sup_adjoin_eps, AddMonoidAlgebra.mem_adjoin_support, adjoin_univ, IsCyclotomicExtension.union_left, adjoin_mono, IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin, adjoin_le_iff, StarAlgebra.adjoin_toSubalgebra, Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le, adjoin_prod_le, AlgHom.adjoin_le_equalizer, restrictScalars_adjoin, EssFiniteType.aux, adjoin_restrictScalars, mem_coeSubmodule_conductor, isCyclotomicExtension_iff, minpoly.equivAdjoin_toAlgHom, adjoin_le, MvPolynomial.irreducible_toPolynomialAdjoinImageCompl, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_right, RingOfIntegers.exponent_eq_one_iff, AlgebraicIndependent.aevalEquiv_apply_coe, RingHom.adjoin_algebraMap_surjective, Subalgebra.adjoin_eq_span_of_eq_span, IsAlgebraic.exists_nonzero_eq_adjoin_mul, IsCyclotomicExtension.iff_adjoin_eq_top, AlgebraicIndependent.option_iff, Polynomial.algEquivOfTranscendental_apply_X, IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin, mem_ideal_map_adjoin, Polynomial.Bivariate.Transcendental.algEquivAdjoin_apply, Polynomial.Bivariate.aeval_aeval_eq_aeval_algEquivAdjoin, adjoin_eq, PolynomialLaw.range_φ, instIsMulCommutative_adjoin, AlgebraicIndependent.matroid_closure_eq, minpoly.coe_equivAdjoin, adjoin.powerBasis'_minpoly_gen, adjoin_eq_range_freeAlgebra_lift, mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt, adjoin_iUnion, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_left, mem_adjoin_of_map_mul, IntermediateField.adjoin_eq_top_iff, IsCyclotomicExtension.Rat.adjoin_singleton_eq_top, IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, adjoin_eq_sInf, adjoin_algebraMap, mem_adjoin_of_dvd_coeff_of_dvd_aeval, IsPrimitiveRoot.self_sub_one_pow_dvd_order, adjoin_eq_top_of_intermediateField, Polynomial.algEquivOfTranscendental_symm_aeval, IsDedekindDomain.adjoin_union_eq_top_of_isCoprime_differentialIdeal, IsPrimitiveRoot.adjoin_isCyclotomicExtension, AddMonoidAlgebra.support_gen_of_gen, conductor_eq_top_iff_adjoin_eq_top, AlgebraicIndependent.iff_adjoin_image, AlgHom.map_adjoin_singleton, AdjoinRoot.adjoinRoot_eq_top, QuaternionAlgebra.Basis.range_liftHom, IntermediateField.algebraicIndependent_adjoin_iff, IsIntegral.fg_adjoin_singleton, cardinalMk_adjoin_le, adjoin_res_eq_adjoin_res, Complex.adjoin_I, IsCyclotomicExtension.adjoin_roots, IntermediateField.algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin, RingHom.adjoinAlgebraMap_apply, IntermediateField.isAlgebraic_adjoin_iff_bot, adjoin_union_eq_adjoin_adjoin, IsTranscendenceBasis.isAlgebraic, adjoin_toSubsemiring, Polynomial.aeval_mem_adjoin_singleton, IntermediateField.transcendental_adjoin_iff, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic, IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1, adjoin.powerBasis'_gen, IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right, isAlgebraic_adjoin_of_nonempty, IsAlgClosed.isAlgClosure_of_transcendence_basis, IsCyclotomicExtension.union_right, IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots, Polynomial.IsSplittingField.adjoin_rootSet_eq_range, IntermediateField.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap, IsIntegral.inv_mem_adjoin, essFiniteType_iff, EssFiniteType.cond, TensorProduct.adjoin_tmul_eq_top, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton, sup_def, Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_right, restrictScalars_adjoin_of_algEquiv, IntermediateField.adjoin_algebraic_toSubalgebra, MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_le, IsAdjoinRoot.adjoin_root_eq_top, AddMonoidAlgebra.support_gen_of_gen', Polynomial.Bivariate.Transcendental.algEquivAdjoin_swap_eq_aeval, CyclotomicRing.eq_adjoin_primitive_root, adjoin_insert_zero, Polynomial.SplittingField.adjoin_rootSet, AlgebraicIndependent.iff_transcendental_adjoin_image, TrivSqZeroExt.range_inlAlgHom_sup_adjoin_range_inr, Polynomial.adjoin_X, adjoin_int, Module.End.exists_isNilpotent_isSemisimple, isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic, StarAlgebra.adjoin_eq_starClosure_adjoin, Subalgebra.topologicalClosure_adjoin_le_centralizer_centralizer, IntermediateField.algebraAdjoinAdjoin.coe_algebraMap, gc, adjoin_empty, mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt, TensorProduct.adjoin_one_tmul_image_eq_top, IntermediateField.algebra_adjoin_le_adjoin, adjoin_eq_of_le, TrivSqZeroExt.range_liftAux, adjoin_nat, comap_map_eq_map_adjoin_of_coprime_conductor, Subalgebra.restrictScalars_adjoin, self_mem_adjoin_singleton, rank_adjoin_le
adjoinCommRingOfComm 📖	CompOp	—
adjoinCommSemiringOfComm 📖	CompOp	—
botEquiv 📖	CompOp	1 math math: botEquiv_symm_apply
botEquivOfInjective 📖	CompOp	—
delabAdjoinNotation 📖	CompOp	—
gi 📖	CompOp	—
instCompleteLatticeSubalgebra 📖	CompOp	281 math math: IsCyclotomicExtension.adjoin_primitive_root_eq_top, range_ofId, Subalgebra.LinearDisjoint.inf_eq_bot, Submodule.rTensorOne_symm_apply, IntermediateField.adjoin_eq_top_iff_of_isAlgebraic, mem_iInf, Subalgebra.coe_iSup_of_directed, Submodule.comm_trans_lTensorOne, IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot, adjoin_singleton_intCast, Subalgebra.LinearDisjoint.sup_free_of_free, Subalgebra.pi_top, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero, mem_top, Submodule.mulMap_one_right_eq, Subalgebra.comap_map_eq, Subalgebra.finrank_sup_eq_finrank_right_mul_finrank_of_free, Subalgebra.op_sSup, TensorAlgebra.adjoin_range_ι, AlgHom.equalizer_eq_top, DualNumber.range_lift, Subalgebra.op_sInf, StarSubalgebra.inf_toSubalgebra, sSup_def, toSubsemiring_eq_top, Subalgebra.op_bot, mem_sInf, adjoin_singleton_algebraMap, Subalgebra.centralizer_coe_iSup, toSubring_eq_top, NumberField.adjoin_eq_top_of_infinitePlace_lt, Subalgebra.rank_sup_eq_rank_left_mul_rank_of_free, Polynomial.IsSplittingField.splits_iff, StarSubalgebra.bot_toSubalgebra, toSubring_bot, integralClosure_eq_top_iff, Subalgebra.LinearDisjoint.inf_eq_bot_of_commute, map_sup, Subalgebra.algebra_isAlgebraic_bot_right, Subalgebra.unop_sup, Subalgebra.comm_trans_rTensorBot, HomogeneousLocalization.Away.adjoin_mk_prod_pow_eq_top, Subalgebra.algebra_isAlgebraic_bot_left_iff, EssFiniteType.adjoin_mem_finset, adjoin_attach_biUnion, Polynomial.IsSplittingField.adjoin_rootSet, Subalgebra.prod_inf_prod, IntermediateField.inf_toSubalgebra, MonoidAlgebra.support_gen_of_gen', Subalgebra.center_eq_top, IsIntegrallyClosedIn.integralClosure_eq_bot, integralClosure_idem, mem_bot, adjoin_union, coe_iInf, Polynomial.SplittingFieldAux.adjoin_rootSet, IntermediateField.bot_toSubalgebra, toSubmodule_bot, map_bot, IntermediateField.sup_toSubalgebra_of_isAlgebraic_left, adjoin_singleton_zero, coe_bot, IsDedekindDomain.range_sup_range_eq_top_of_isCoprime_differentIdeal, sInf_toSubsemiring, sInf_toSubmodule, MvPolynomial.adjoin_range_X, IsDedekindDomain.integer_empty, adjoin_eq_top_of_conductor_eq_top, Subalgebra.eq_bot_of_finrank_one, Subalgebra.LinearDisjoint.rank_sup_of_free, coe_top, Subalgebra.unop_top, Subalgebra.lTensorBot_one_tmul, Subalgebra.isSimpleOrder_of_finrank, Subalgebra.mulMap_bot_left_eq, Subalgebra.op_inf, Polynomial.adjoin_rootSet_eq_range, IntermediateField.sup_toSubalgebra_of_isAlgebraic, top_toSubmodule, Subalgebra.fg_of_submodule_fg, CliffordAlgebra.adjoin_range_ι, Polynomial.Splits.adjoin_rootSet_eq_range, IntermediateField.sInf_toSubalgebra, map_inf, sup_toSubsemiring, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous, Subalgebra.mem_starClosure, Subalgebra.finrank_right_dvd_finrank_sup_of_free, PrimeSpectrum.iInf_localization_eq_bot, Subalgebra.mul_toSubmodule, Subalgebra.unop_bot, bijective_algebraMap_iff, Subalgebra.topEquiv_apply, IntermediateField.adjoin_simple_eq_top_iff_of_isAlgebraic, iSup_toSubsemiring, PowerBasis.adjoin_gen_eq_top, Subalgebra.mulMap'_surjective, Submodule.comm_trans_rTensorOne, mem_sup_left, top_toSubring, IntermediateField.top_toSubalgebra, Subalgebra.finrank_left_dvd_finrank_sup_of_free, Submodule.lTensorOne'_tmul, Submodule.rTensorOne'_tmul_one, Subalgebra.unop_sSup, Submodule.rTensorOne'_tmul, Subalgebra.mul_toSubmodule_le, DenseRange.topologicalClosure_map_subalgebra, adjoin_eq_top_of_primitive_element, zariskisMainProperty_iff_exists_saturation_eq_top, MonoidAlgebra.exists_finset_adjoin_eq_top, sSup_toSubsemiring, IsIntegrallyClosed.iInf, TensorProduct.productMap_range, PowerBasis.adjoin_eq_top_of_gen_mem_adjoin, IsIntegrallyClosed.integralClosure_eq_bot, IsIntegrallyClosed.integralClosure_eq_bot_iff, Polynomial.IsSplittingField.adjoin_rootSet', Submodule.rTensorOne_tmul, Subalgebra.unop_iInf, inf_toSubmodule, AlgHom.range_eq_top, adjoin_singleton_one, iInf_toSubsemiring, Subalgebra.centralizer_eq_top_iff_subset, Subalgebra.unop_inf, top_toSubsemiring, Subalgebra.rTensorBot_tmul_one, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_of_inj, Subalgebra.finrank_sup_eq_finrank_left_mul_finrank_of_free, IsIntegrallyClosedIn.integralClosure_eq_bot_iff, Subalgebra.finrank_sup_le_of_free, Subalgebra.starClosure_toSubalgebra, Submodule.rTensorOne_tmul_one, fg_trans', Subalgebra.op_top, adjoin_singleton_natCast, Subalgebra.finite_sup, Subalgebra.op_iInf, Subalgebra.bot_eq_top_iff_finrank_eq_one, Subalgebra.mulMap_bot_right_eq, AddMonoidAlgebra.exists_finset_adjoin_eq_top, iInf_toSubmodule, Subalgebra.rank_sup_eq_rank_right_mul_rank_of_free, isAlgebraic_iff, Subalgebra.lTensorBot_symm_apply, FreeAlgebra.adjoin_range_ι, ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, TensorProduct.map_range, IntermediateField.sup_toSubalgebra_of_left, StarSubalgebra.toSubalgebra_eq_top, Submodule.mulMap_one_left_eq, MonoidAlgebra.support_gen_of_gen, adjoin_adjoin_coe_preimage, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_left_of_inj, adjoin_top, Subalgebra.FG.sup, adjoin_root_eq_top_of_isSplittingField, Subalgebra.LinearDisjoint.finrank_sup_of_free, surjective_algebraMap_iff, toSubmodule_eq_top, DualNumber.range_inlAlgHom_sup_adjoin_eps, Subalgebra.fg_bot, adjoin_univ, AlgHom.equalizer_same, Subalgebra.fg_top, EssFiniteType.aux, IntermediateField.topEquiv_symm_apply_coe, Subalgebra.lTensorBot_tmul, Subalgebra.topEquiv_symm_apply_coe, isIntegral_iSup, Subalgebra.rank_sup_le_of_free, IntermediateField.topEquiv_apply, isIntegral_sup, Subalgebra.op_iSup, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_of_inj, IsCyclotomicExtension.singleton_one, Subalgebra.op_sup, adjoin_restrictScalars, Subalgebra.LinearDisjoint.val_mulMap_tmul, Subalgebra.mulMap_range, RingOfIntegers.exponent_eq_one_iff, Subalgebra.rTensorBot_symm_apply, comap_top, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_right_of_inj, StarSubalgebra.sInf_toSubalgebra, MaximalSpectrum.iInf_localization_eq_bot, IsCentral.center_eq_bot, mem_iSup_of_mem, Subalgebra.centralizer_coe_sup, Submodule.lTensorOne_symm_apply, MvPolynomial.supported_empty, IsCyclotomicExtension.iff_adjoin_eq_top, Subalgebra.coe_starClosure, JacobsonNoether.exists_separable_and_not_isCentral', IntermediateField.toSubalgebra_iSup_of_directed, Submodule.lTensorOne'_one_tmul, eq_top_iff, adjoin_iUnion, Subalgebra.rank_eq_one_iff, Subalgebra.prod_top, Subalgebra.map_comap_eq, subalgebra_top_finrank_eq_submodule_top_finrank, IntermediateField.adjoin_eq_top_iff, Valuation.Integers.integralClosure, IsCyclotomicExtension.Rat.adjoin_singleton_eq_top, mem_sup_right, IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, polynomialFunctions.topologicalClosure, RingCon.range_mkₐ, adjoin_eq_sInf, map_top, Subalgebra.eq_bot_of_rank_le_one, Submodule.lTensorOne_tmul, coe_inf, Subalgebra.comm_trans_lTensorBot, adjoin_eq_top_of_intermediateField, IsDedekindDomain.adjoin_union_eq_top_of_isCoprime_differentialIdeal, Subalgebra.bot_eq_top_of_finrank_eq_one, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_left_of_inj, AddMonoidAlgebra.support_gen_of_gen, MvPolynomial.supported_univ, conductor_eq_top_iff_adjoin_eq_top, Subalgebra.isAlgebraic_bot_iff, AdjoinRoot.adjoinRoot_eq_top, Subalgebra.isSimpleOrder_of_finrank_prime, mul_mem_sup, Complex.adjoin_I, FiniteType.out, polynomialFunctions_closure_eq_top', Subalgebra.val_mulMap'_tmul, IntermediateField.sup_toSubalgebra_of_right, AlgHom.eqOn_sup, IntermediateField.le_sup_toSubalgebra, IntermediateField.sup_toSubalgebra_of_isAlgebraic_right, Submodule.lTensorOne_one_tmul, map_iInf, TensorProduct.adjoin_tmul_eq_top, IntermediateField.iInf_toSubalgebra, mem_inf, Subalgebra.LinearDisjoint.eq_bot_of_commute_of_self, Subalgebra.finrank_bot, coe_sInf, sup_def, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_right_of_inj, Subalgebra.restrictScalars_top, IsCentral.out, polynomialFunctions_closure_eq_top, IsDedekindDomain.integer_univ, IsAdjoinRoot.adjoin_root_eq_top, AddMonoidAlgebra.support_gen_of_gen', Subalgebra.bot_eq_top_iff_rank_eq_one, Subalgebra.rTensorBot_tmul, range_id, Polynomial.SplittingField.adjoin_rootSet, TrivSqZeroExt.range_inlAlgHom_sup_adjoin_range_inr, Polynomial.adjoin_X, inf_toSubsemiring, StarSubalgebra.iInf_toSubalgebra, StarSubalgebra.top_toSubalgebra, IsCyclotomicExtension.lcm_sup, Subalgebra.LinearDisjoint.eq_bot_of_self, Subalgebra.LinearDisjoint.bot_left, Subalgebra.rank_bot, Subalgebra.LinearDisjoint.bot_right, notMem_iff_exists_ne_and_isConjRoot, adjoin_empty, Subalgebra.fg_bot_toSubmodule, botEquiv_symm_apply, Subalgebra.rank_top, Subalgebra.bot_eq_top_of_rank_eq_one, fg_of_fg_of_fg, TensorProduct.adjoin_one_tmul_image_eq_top, Subalgebra.finrank_eq_one_iff, subalgebra_top_rank_eq_submodule_top_rank, TrivSqZeroExt.range_liftAux, Subalgebra.eq_bot_of_isPurelyInseparable_of_isSeparable, Subalgebra.finite_bot, Subalgebra.restrictScalars_adjoin, Subalgebra.unop_iSup, Subalgebra.unop_sInf
instInhabitedSubalgebra 📖	CompOp	—
instSubtypeMemSubalgebraMin 📖	CompOp	—
instSubtypeMemSubalgebraMin_1 📖	CompOp	—
subalgebra_adjoin 📖	CompOp	—
toTop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_adjoin_coe_preimage 📖	mathematical	—	adjoin Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.toSemiring Subalgebra.algebra Set.preimage Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	eq_top_iff adjoin_induction subset_adjoin Subalgebra.algebraMap_mem Subalgebra.add_mem Subalgebra.mul_mem
adjoin_attach_biUnion 📖	mathematical	—	adjoin SetLike.coe Finset Finset.instSetLike Finset.biUnion SetLike.instMembership Finset.attach iSup Subalgebra ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	Finset.coe_biUnion Set.iUnion_congr_Prop Finset.coe_attach Set.iUnion_true adjoin_iUnion
adjoin_empty 📖	mathematical	—	adjoin Set Set.instEmptyCollection Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	GaloisConnection.l_bot gc
adjoin_eq 📖	mathematical	—	adjoin SetLike.coe Subalgebra Subalgebra.instSetLike	—	adjoin_eq_of_le Set.Subset.refl subset_adjoin
adjoin_eq_of_le 📖	mathematical	Set Set.instHasSubset SetLike.coe Subalgebra Subalgebra.instSetLike Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder adjoin	adjoin	—	le_antisymm adjoin_le
adjoin_eq_ring_closure 📖	mathematical	—	Subalgebra.toSubring adjoin CommRing.toCommSemiring Ring.toSemiring Subring.closure Ring.toNonAssocRing Set Set.instUnion Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	Subring.closure_eq_of_le Subsemiring.closure_induction Subring.subset_closure Subring.zero_mem Subring.one_mem Subring.add_mem Subring.mul_mem
adjoin_eq_sInf 📖	mathematical	—	adjoin InfSet.sInf Subalgebra ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra setOf Set Set.instHasSubset SetLike.coe Subalgebra.instSetLike	—	le_antisymm le_sInf adjoin_le sInf_le subset_adjoin
adjoin_eq_span 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule adjoin Submodule.span SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike Submonoid.closure	—	le_antisymm Subsemiring.mem_closure_iff_exists_list ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Submodule.add_mem Submonoid.one_mem' one_smul smul_def RingHom.map_mul mul_assoc Submonoid.mul_mem Submonoid.subset_closure mul_smul_comm to_smulCommClass Submodule.smul_mem Submodule.subset_span Submodule.span_le Submonoid.closure_le subset_adjoin
adjoin_eq_span_of_subset 📖	mathematical	Set Set.instHasSubset SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Submonoid.instSetLike Submonoid.closure Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring toModule Submodule.setLike Submodule.span	DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule adjoin Submodule.span	—	le_antisymm adjoin_toSubmodule_le span_le_adjoin
adjoin_iUnion 📖	mathematical	—	adjoin Set.iUnion iSup Subalgebra ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	GaloisConnection.l_iSup gc
adjoin_image 📖	mathematical	—	adjoin Set.image DFunLike.coe AlgHom AlgHom.funLike Subalgebra.map	—	le_antisymm adjoin_le Set.image_mono subset_adjoin Subalgebra.map_le Set.image_subset_iff Set.image_id'
adjoin_induction 📖	—	subset_adjoin DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap algebraMap_mem Subalgebra Subalgebra.instSetLike AddSubmonoidWithOneClass.toOneMemClass AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass Subalgebra.instSMulMemClass adjoin Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid SubsemiringClass.toAddSubmonoidClass Distrib.toMul MulMemClass.mul_mem SubmonoidClass.toMulMemClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SubsemiringClass.toSubmonoidClass SetLike.instMembership	—	—	subset_adjoin algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass Subalgebra.instSMulMemClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass RingHom.map_one RingHom.map_zero adjoin_le
adjoin_induction₂ 📖	—	subset_adjoin DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap algebraMap_mem Subalgebra Subalgebra.instSetLike AddSubmonoidWithOneClass.toOneMemClass AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass Subalgebra.instSMulMemClass adjoin Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid SubsemiringClass.toAddSubmonoidClass Distrib.toMul MulMemClass.mul_mem SubmonoidClass.toMulMemClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SubsemiringClass.toSubmonoidClass SetLike.instMembership	—	—	subset_adjoin algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass Subalgebra.instSMulMemClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass adjoin_induction
adjoin_insert_adjoin 📖	mathematical	—	adjoin Set Set.instInsert SetLike.coe Subalgebra Subalgebra.instSetLike	—	le_antisymm adjoin_le Set.insert_subset_iff subset_adjoin Set.mem_insert adjoin_mono Set.subset_insert Set.insert_subset_insert
adjoin_insert_algebraMap 📖	mathematical	—	adjoin Set Set.instInsert DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	Set.insert_eq adjoin_union adjoin_singleton_algebraMap sup_of_le_right
adjoin_insert_intCast 📖	mathematical	—	adjoin CommRing.toCommSemiring Ring.toSemiring Set Set.instInsert AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	map_intCast RingHom.instRingHomClass adjoin_insert_algebraMap
adjoin_insert_natCast 📖	mathematical	—	adjoin Set Set.instInsert AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	algebraMap.coe_natCast adjoin_insert_algebraMap
adjoin_insert_one 📖	mathematical	—	adjoin Set Set.instInsert AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	Nat.cast_one adjoin_insert_natCast
adjoin_insert_zero 📖	mathematical	—	adjoin Set Set.instInsert MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Nat.cast_zero adjoin_insert_natCast
adjoin_int 📖	mathematical	—	adjoin Int.instCommSemiring Ring.toSemiring Ring.toIntAlgebra subalgebraOfSubring Subring.closure Ring.toNonAssocRing	—	le_antisymm adjoin_le Subring.subset_closure Subring.closure_le subset_adjoin
adjoin_le 📖	mathematical	Set Set.instHasSubset SetLike.coe Subalgebra Subalgebra.instSetLike	Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder adjoin	—	GaloisConnection.l_le gc
adjoin_le_centralizer_centralizer 📖	mathematical	—	Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder adjoin Subalgebra.centralizer SetLike.coe Subalgebra.instSetLike	—	adjoin_le Set.subset_centralizer_centralizer
adjoin_le_iff 📖	mathematical	—	Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder adjoin Set Set.instHasSubset SetLike.coe Subalgebra.instSetLike	—	gc
adjoin_mono 📖	mathematical	Set Set.instHasSubset	Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder adjoin	—	GaloisConnection.monotone_l gc
adjoin_nat 📖	mathematical	—	adjoin Nat.instCommSemiring Semiring.toNatAlgebra subalgebraOfSubsemiring Subsemiring.closure Semiring.toNonAssocSemiring	—	le_antisymm adjoin_le Subsemiring.subset_closure Subsemiring.closure_le subset_adjoin
adjoin_nonUnitalSubalgebra 📖	mathematical	—	adjoin Ring.toSemiring SetLike.coe NonUnitalSubalgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toModule NonUnitalSubalgebra.instSetLike NonUnitalAlgebra.adjoin IsScalarTower.right to_smulCommClass	—	le_antisymm IsScalarTower.right to_smulCommClass adjoin_le NonUnitalAlgebra.adjoin_le_algebra_adjoin HasSubset.Subset.trans Set.instIsTransSubset NonUnitalAlgebra.subset_adjoin subset_adjoin
adjoin_singleton_algebraMap 📖	mathematical	—	adjoin Set Set.instSingletonSet DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	bot_unique adjoin_singleton_le Subalgebra.algebraMap_mem
adjoin_singleton_intCast 📖	mathematical	—	adjoin CommRing.toCommSemiring Ring.toSemiring Set Set.instSingletonSet AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	map_intCast RingHom.instRingHomClass adjoin_singleton_algebraMap
adjoin_singleton_le 📖	mathematical	Subalgebra SetLike.instMembership Subalgebra.instSetLike	Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder adjoin Set Set.instSingletonSet	—	adjoin_le Set.singleton_subset_iff
adjoin_singleton_natCast 📖	mathematical	—	adjoin Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	map_natCast RingHom.instRingHomClass adjoin_singleton_algebraMap
adjoin_singleton_one 📖	mathematical	—	adjoin Set Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Nat.cast_one adjoin_singleton_natCast
adjoin_singleton_zero 📖	mathematical	—	adjoin Set Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Nat.cast_zero adjoin_singleton_natCast
adjoin_span 📖	mathematical	—	adjoin SetLike.coe Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Submodule.setLike Submodule.span	—	le_antisymm adjoin_le span_le_adjoin adjoin_mono Submodule.subset_span
adjoin_toSubmodule_le 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder DFunLike.coe OrderEmbedding Subalgebra Subalgebra.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule adjoin Set Set.instHasSubset SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike Submonoid.closure Submodule.setLike	—	adjoin_eq_span Submodule.span_le
adjoin_toSubsemiring 📖	mathematical	—	Subalgebra.toSubsemiring adjoin Subsemiring.closure Semiring.toNonAssocSemiring Set Set.instUnion Set.range DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
adjoin_union 📖	mathematical	—	adjoin Set Set.instUnion Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	GaloisConnection.l_sup gc
adjoin_union_coe_submodule 📖	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 Set Set.instUnion Submodule.mul IsScalarTower.right	—	IsScalarTower.right adjoin_eq_span Submodule.span_mul_span Set.ext Submonoid.closure_union
adjoin_univ 📖	mathematical	—	adjoin Set.univ Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	GaloisInsertion.l_top
bijective_algebraMap_iff 📖	mathematical	—	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield RingHom.instFunLike algebraMap Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Bot.bot OrderBot.toBot BoundedOrder.toOrderBot	—	surjective_algebraMap_iff RingHom.injective DivisionRing.isSimpleRing
botEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Subalgebra Semifield.toCommSemiring Field.toSemifield SetLike.instMembership Subalgebra.instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subalgebra.toSemiring id Subalgebra.algebra AlgEquiv.instFunLike AlgEquiv.symm botEquiv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
coe_bot 📖	mathematical	—	SetLike.coe Subalgebra Subalgebra.instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
coe_iInf 📖	mathematical	—	SetLike.coe Subalgebra Subalgebra.instSetLike iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Set.iInter	—	coe_sInf Set.iInter_congr_Prop Set.iInter_exists Set.iInter_iInter_eq'
coe_inf 📖	mathematical	—	SetLike.coe Subalgebra Subalgebra.instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Set Set.instInter	—	—
coe_sInf 📖	mathematical	—	SetLike.coe Subalgebra Subalgebra.instSetLike InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Set.iInter Set Set.instMembership	—	sInf_image
coe_top 📖	mathematical	—	SetLike.coe Subalgebra Subalgebra.instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.univ	—	—
comap_top 📖	mathematical	—	Subalgebra.comap Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	eq_top_iff mem_top
commute_of_mem_adjoin_of_forall_mem_commute 📖	mathematical	Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	adjoin_induction commutes Commute.add_right Commute.mul_right
commute_of_mem_adjoin_self 📖	mathematical	Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	commute_of_mem_adjoin_singleton_of_commute
commute_of_mem_adjoin_singleton_of_commute 📖	mathematical	Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	commute_of_mem_adjoin_of_forall_mem_commute
eq_top_iff 📖	mathematical	—	Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder SetLike.instMembership Subalgebra.instSetLike	—	mem_top Subalgebra.ext
forall_mem_adjoin_smul_eq_self_iff 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	AlgHom.eqOn_adjoin_iff
gc 📖	mathematical	—	GaloisConnection Set Subalgebra PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Subalgebra.instPartialOrder adjoin SetLike.coe Subalgebra.instSetLike	—	le_trans Set.subset_union_right Subsemiring.subset_closure Subsemiring.closure_le Set.union_subset Subalgebra.range_subset
iInf_toSubmodule 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Submodule.instInfSet	—	SetLike.coe_injective coe_iInf Submodule.coe_iInf
iInf_toSubsemiring 📖	mathematical	—	Subalgebra.toSubsemiring iInf Subalgebra ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Subsemiring Semiring.toNonAssocSemiring Subsemiring.instInfSet	—	sInf_toSubsemiring
iSup_induction 📖	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—	RingHom.map_one RingHom.map_zero iSup_le_iff
iSup_induction' 📖	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra mem_iSup_of_mem Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass Distrib.toMul MulMemClass.mul_mem SubmonoidClass.toMulMemClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SubsemiringClass.toSubmonoidClass DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap Subalgebra.algebraMap_mem	—	—	mem_iSup_of_mem AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass Subalgebra.algebraMap_mem iSup_induction
iSup_toSubsemiring 📖	mathematical	—	Subalgebra.toSubsemiring iSup Subalgebra ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Subsemiring Semiring.toNonAssocSemiring Subsemiring.instCompleteLattice	—	sSup_toSubsemiring
inf_toSubmodule 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Submodule.instMin	—	—
inf_toSubsemiring 📖	mathematical	—	Subalgebra.toSubsemiring Subalgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Subsemiring Semiring.toNonAssocSemiring Subsemiring.instMin	—	—
instIsMulCommutative_adjoin 📖	mathematical	—	IsMulCommutative Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin SetLike.coe Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra.toSemiring	—	isMulCommutative_adjoin setLike_mul_comm
isMulCommutative_adjoin 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	IsMulCommutative Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra.toSemiring	—	adjoin_le_centralizer_centralizer IsMulCommutative.of_setLike_mul_comm SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass Subalgebra.instSubsemiringClass Set.centralizer_centralizer_comm_of_comm
isMulCommutative_adjoin_singleton 📖	mathematical	—	IsMulCommutative Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra.toSemiring	—	isMulCommutative_adjoin
map_bot 📖	mathematical	—	Subalgebra.map Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Subalgebra.toSubmodule_injective RingHomSurjective.ids Subalgebra.map_toSubmodule Submodule.map.congr_simp toSubmodule_bot Submodule.map_one
map_iInf 📖	mathematical	DFunLike.coe AlgHom AlgHom.funLike	Subalgebra.map iInf Subalgebra ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	SetLike.coe_injective coe_iInf Set.InjOn.image_iInter_eq Set.injOn_of_injective
map_inf 📖	mathematical	DFunLike.coe AlgHom AlgHom.funLike	Subalgebra.map Subalgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	SetLike.coe_injective Set.image_inter
map_sup 📖	mathematical	—	Subalgebra.map Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	GaloisConnection.l_sup Subalgebra.gc_map_comap
map_top 📖	mathematical	—	Subalgebra.map Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgHom.range	—	SetLike.coe_injective Set.image_univ
mem_adjoin_iff 📖	mathematical	—	Subalgebra CommRing.toCommSemiring Ring.toSemiring SetLike.instMembership Subalgebra.instSetLike adjoin Subring Ring.toNonAssocRing Subring.instSetLike Subring.closure Set Set.instUnion Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	Subalgebra.mem_toSubring adjoin_eq_ring_closure
mem_adjoin_of_map_mul 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring toModule LinearMap.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin	Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Set.image DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring toModule LinearMap.instFunLike Set Set.instUnion Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	adjoin_induction subset_adjoin Set.subset_union_left Set.subset_union_right Set.mem_singleton algebraMap_eq_smul_one LinearMap.map_smul Subalgebra.smul_mem Set.union_singleton map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Subalgebra.add_mem Subalgebra.mul_mem
mem_adjoin_of_mem 📖	mathematical	Set Set.instMembership	Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin	—	subset_adjoin
mem_bot 📖	mathematical	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
mem_iInf 📖	mathematical	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	—
mem_iSup_of_mem 📖	mathematical	Subalgebra SetLike.instMembership Subalgebra.instSetLike	Subalgebra SetLike.instMembership Subalgebra.instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	le_iSup
mem_inf 📖	mathematical	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	—
mem_sInf 📖	mathematical	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	coe_sInf
mem_sup_left 📖	mathematical	Subalgebra SetLike.instMembership Subalgebra.instSetLike	Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	le_sup_left
mem_sup_right 📖	mathematical	Subalgebra SetLike.instMembership Subalgebra.instSetLike	Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	le_sup_right
mem_top 📖	mathematical	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Set.mem_univ
mul_mem_sup 📖	mathematical	Subalgebra SetLike.instMembership Subalgebra.instSetLike	Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Subalgebra.mul_mem mem_sup_left mem_sup_right
range_id 📖	mathematical	—	AlgHom.range AlgHom.id Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	SetLike.coe_injective Set.range_id
range_ofId 📖	mathematical	—	AlgHom.range CommSemiring.toSemiring id ofId Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
sInf_toSubmodule 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Submodule.instInfSet Set.image	—	SetLike.coe_injective coe_sInf Set.iInter_congr_Prop Set.iInter_exists Set.biInter_and' Set.iInter_iInter_eq_right
sInf_toSubsemiring 📖	mathematical	—	Subalgebra.toSubsemiring InfSet.sInf Subalgebra ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Subsemiring Semiring.toNonAssocSemiring Subsemiring.instInfSet Set.image	—	SetLike.coe_injective coe_sInf Set.iInter_congr_Prop Set.iInter_exists Set.biInter_and' Set.iInter_iInter_eq_right
sSup_def 📖	mathematical	—	SupSet.sSup Subalgebra ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra adjoin Set.sUnion Set.image Set SetLike.coe Subalgebra.instSetLike	—	—
sSup_toSubsemiring 📖	mathematical	Set.Nonempty Subalgebra	Subalgebra.toSubsemiring SupSet.sSup Subalgebra ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Subsemiring Semiring.toNonAssocSemiring Subsemiring.instCompleteLattice Set.image	—	Set.image_image Set.image_congr Subsemiring.closure_eq sSup_image Subsemiring.closure_sUnion sSup_def adjoin_toSubsemiring Set.union_eq_right algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass Subalgebra.instSMulMemClass
self_mem_adjoin_singleton 📖	mathematical	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet	—	subset_adjoin Set.mem_singleton_iff
span_le_adjoin 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.span DFunLike.coe OrderEmbedding Subalgebra Subalgebra.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule adjoin	—	Submodule.span_le subset_adjoin
subset_adjoin 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Subalgebra Subalgebra.instSetLike adjoin	—	GaloisConnection.le_u_l gc
sup_def 📖	mathematical	—	Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra adjoin Set Set.instUnion SetLike.coe Subalgebra.instSetLike	—	—
sup_toSubsemiring 📖	mathematical	—	Subalgebra.toSubsemiring Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Subsemiring Semiring.toNonAssocSemiring Subsemiring.instCompleteLattice	—	Subsemiring.closure_eq Subsemiring.closure_union Set.union_eq_right Set.mem_union_left algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass Subalgebra.instSMulMemClass
surjective_algebraMap_iff 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Bot.bot OrderBot.toBot BoundedOrder.toOrderBot	—	eq_bot_iff Subalgebra.algebraMap_mem mem_bot mem_top
toSubmodule_bot 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule Bot.bot OrderBot.toBot SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Submodule.one	—	RingHomSurjective.ids Submodule.one_eq_range
toSubmodule_eq_top 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule Top.top Submodule.instTop OrderTop.toTop SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	RelEmbedding.injective top_toSubmodule
toSubring_bot 📖	mathematical	—	Subalgebra.toSubring Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing SetLike.instMembership Subring.instSetLike Subring.toCommRing CommRing.toRing ofSubring id CommRing.toCommSemiring Bot.bot Subalgebra SubsemiringClass.toCommSemiring SubringClass.toSubsemiringClass Subring.instSubringClass CommSemiring.toSemiring OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Subring.ext SubringClass.toSubsemiringClass Subring.instSubringClass Subalgebra.neg_mem Subalgebra.mem_carrier
toSubring_eq_top 📖	mathematical	—	Subalgebra.toSubring Top.top Subring Ring.toNonAssocRing Subring.instTop Subalgebra CommRing.toCommSemiring Ring.toSemiring OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Subalgebra.toSubring_injective top_toSubring
toSubsemiring_eq_top 📖	mathematical	—	Subalgebra.toSubsemiring Top.top Subsemiring Semiring.toNonAssocSemiring Subsemiring.instTop Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Subalgebra.toSubsemiring_injective top_toSubsemiring
top_toSubmodule 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule Top.top OrderTop.toTop SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Submodule.instTop	—	—
top_toSubring 📖	mathematical	—	Subalgebra.toSubring Top.top Subalgebra CommRing.toCommSemiring Ring.toSemiring OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Subring Ring.toNonAssocRing Subring.instTop	—	—
top_toSubsemiring 📖	mathematical	—	Subalgebra.toSubsemiring Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Subsemiring Semiring.toNonAssocSemiring Subsemiring.instTop	—	—

NonUnitalAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_le_algebra_adjoin 📖	mathematical	—	NonUnitalSubalgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring Preorder.toLE PartialOrder.toPreorder NonUnitalSubalgebra.instPartialOrder adjoin IsScalarTower.right Algebra.to_smulCommClass Subalgebra.toNonUnitalSubalgebra Algebra.adjoin	—	adjoin_le IsScalarTower.right Algebra.to_smulCommClass Algebra.subset_adjoin

Subalgebra

Definitions

Name	Category	Theorems
instUnique 📖	CompOp	—
saturation 📖	CompOp	6 math math: mem_saturation_of_mul_mem_right, mem_saturation_of_mul_mem_left, mem_saturation_iff, Algebra.zariskisMainProperty_iff_exists_saturation_eq_top, saturation_saturation, le_saturation
toNonUnitalSubalgebraOrderEmbedding 📖	CompOp	—
topEquiv 📖	CompOp	2 math math: topEquiv_apply, topEquiv_symm_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_eq_span_of_eq_span 📖	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 Submodule.span	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	—	Submonoid.adjoin_eq_span_of_eq_span
center_eq_top 📖	mathematical	—	center CommSemiring.toSemiring Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	SetLike.coe_injective Set.center_eq_univ
centralizer_eq_top_iff_subset 📖	mathematical	—	centralizer Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set Set.instHasSubset SetLike.coe instSetLike center	—	SetLike.ext'_iff Set.centralizer_eq_top_iff_subset
comap_map_eq 📖	mathematical	—	comap Ring.toSemiring map Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Algebra.adjoin Set.preimage DFunLike.coe AlgHom AlgHom.funLike Set Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	le_antisymm mem_map mem_comap map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass sub_self Algebra.adjoin_eq Algebra.adjoin_union add_sub_cancel add_mem Algebra.subset_adjoin map_le Algebra.map_sup AlgHom.map_adjoin le_of_eq sup_eq_left Algebra.adjoin_le_iff HasSubset.Subset.trans Set.instIsTransSubset Set.image_preimage_subset Set.singleton_subset_iff zero_mem
comap_map_eq_self 📖	mathematical	Set Set.instHasSubset Set.preimage DFunLike.coe AlgHom Ring.toSemiring AlgHom.funLike Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SetLike.coe Subalgebra instSetLike	comap Ring.toSemiring map	—	left_eq_sup Algebra.adjoin_le_iff comap_map_eq
le_saturation 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Subsemiring.toSubmonoid toSubsemiring	Subalgebra CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder saturation	—	OneMemClass.one_mem SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass one_mul
map_comap_eq 📖	mathematical	—	map comap Subalgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra AlgHom.range	—	SetLike.coe_injective Set.image_preimage_eq_inter_range
map_comap_eq_self 📖	mathematical	Subalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder AlgHom.range	map comap	—	inf_of_le_left map_comap_eq
map_comap_eq_self_of_surjective 📖	mathematical	DFunLike.coe AlgHom AlgHom.funLike	map comap	—	map_comap_eq_self AlgHom.range_eq_top
mem_saturation_iff 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Subsemiring.toSubmonoid toSubsemiring	Subalgebra CommSemiring.toSemiring SetLike.instMembership instSetLike saturation Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Submonoid.instSetLike Algebra.toSMul Algebra.id	—	—
mem_saturation_of_mul_mem_left 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Subsemiring.toSubmonoid toSubsemiring Subalgebra SetLike.instMembership instSetLike saturation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Submonoid.instSetLike	Subalgebra CommSemiring.toSemiring SetLike.instMembership instSetLike saturation	—	Eq.le LE.le.trans le_saturation saturation_saturation
mem_saturation_of_mul_mem_right 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Subsemiring.toSubmonoid toSubsemiring Subalgebra SetLike.instMembership instSetLike saturation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Submonoid.instSetLike	Subalgebra CommSemiring.toSemiring SetLike.instMembership instSetLike saturation	—	mem_saturation_of_mul_mem_left mul_comm
saturation_saturation 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Subsemiring.toSubmonoid toSubsemiring	saturation LE.le.trans Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring PartialOrder.toPreorder Submonoid.instPartialOrder Subsemiring.toSubmonoid toSubsemiring le_saturation	—	LE.le.antisymm' LE.le.trans le_saturation Submonoid.mul_mem mul_assoc
toNonUnitalSubalgebra_le_toNonUnitalSubalgebra 📖	mathematical	—	NonUnitalSubalgebra NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder NonUnitalSubalgebra.instPartialOrder toNonUnitalSubalgebra Subalgebra instPartialOrder	—	OrderEmbedding.le_iff_le
toNonUnitalSubalgebra_mono 📖	mathematical	Subalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	NonUnitalSubalgebra NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder NonUnitalSubalgebra.instPartialOrder toNonUnitalSubalgebra	—	toNonUnitalSubalgebra_le_toNonUnitalSubalgebra
topEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Subalgebra SetLike.instMembership instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder toSemiring algebra AlgEquiv.instFunLike topEquiv	—	—
topEquiv_symm_apply_coe 📖	mathematical	—	Subalgebra SetLike.instMembership instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe AlgEquiv toSemiring algebra AlgEquiv.instFunLike AlgEquiv.symm topEquiv	—	—

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_eq_span_of_eq_span 📖	mathematical	SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSetLike Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.setLike Submodule.span	DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule Algebra.adjoin SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instSetLike Submodule.span	—	Algebra.adjoin_eq_span closure_eq LE.le.antisymm Submodule.span_le Submodule.span_subset_span Submodule.span_mono Submodule.subset_span

Subring

Definitions

Name	Category	Theorems
closureEquivAdjoinInt 📖	CompOp	—

Subsemiring

Definitions

Name	Category	Theorems
closureEquivAdjoinNat 📖	CompOp	—

---

← Back to Index