Lattice

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

Statistics

Metric	Count
Definitions adjoin, adjoinCommRingOfComm, adjoinCommSemiringOfComm, botEquiv, botEquivOfInjective, gi, instCompleteLatticeSubalgebra, instInhabitedSubalgebra, instSubtypeMemSubalgebraMin, instSubtypeMemSubalgebraMin_1, toTop, instUnique, saturation, topEquiv, closureEquivAdjoinInt, closureEquivAdjoinNat	16
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, 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, topEquiv_apply, topEquiv_symm_apply_coe, adjoin_eq_span_of_eq_span	128
Total	144

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 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	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	284 math math: 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, 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, 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, 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, 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, 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, adjoin_insert_one, AlgebraicIndependent.sumElim_iff, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime, span_coeff_minpolyDiv, 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, FractionalIdeal.adjoinIntegral_coe, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, adjoin_nonUnitalSubalgebra_eq_span, adjoin_insert_algebraMap, isNoetherian_adjoin_finset, adjoin_singleton_eq_range_aeval, 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, Complex.range_liftAux, Subalgebra.adjoin_eq_span_basis, adjoin.powerBasis'_dim, AlgebraicIndependent.isAlgebraic_adjoin_iff_of_matroid_isBasis, IntermediateField.mem_adjoin_iff_div, 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, Polynomial.IsSplittingField.adjoin_rootSet', AlgHom.map_adjoin, 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, AlgebraicIndependent.algebraMap_aevalEquiv, AdjoinRoot.Minpoly.coe_toAdjoin_mk_X, IsCyclotomicExtension.iff_singleton, adjoin_range_eq_range_aeval, MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero, 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, 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_ι, isAlgebraic_iff_exists_isTranscendenceBasis_subset, adjoin_union_coe_submodule, isCyclotomicExtension_singleton_iff_eq_adjoin, AlgebraicIndependent.aeval_repr, AlgHom.eqOn_adjoin_iff, adjoin_adjoin_coe_preimage, fg_adjoin_of_finite, adjoin_top, 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, 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, IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin, mem_ideal_map_adjoin, adjoin_eq, PolynomialLaw.range_φ, AlgebraicIndependent.matroid_closure_eq, minpoly.coe_equivAdjoin, adjoin.powerBasis'_minpoly_gen, adjoin_eq_range_freeAlgebra_lift, adjoin_iUnion, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_left, 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, IsPrimitiveRoot.adjoin_isCyclotomicExtension, 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, Complex.adjoin_I, IsCyclotomicExtension.adjoin_roots, IntermediateField.algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin, 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, 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, gc, adjoin_empty, IntermediateField.algebra_adjoin_le_adjoin, TrivSqZeroExt.range_liftAux, adjoin_nat, Subalgebra.restrictScalars_adjoin, self_mem_adjoin_singleton, rank_adjoin_le
adjoinCommRingOfComm 📖	CompOp	—
adjoinCommSemiringOfComm 📖	CompOp	—
botEquiv 📖	CompOp	1 math math: botEquiv_symm_apply
botEquivOfInjective 📖	CompOp	—
gi 📖	CompOp	—
instCompleteLatticeSubalgebra 📖	CompOp	266 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, map_sup, Subalgebra.algebra_isAlgebraic_bot_right, Subalgebra.unop_sup, Subalgebra.comm_trans_rTensorBot, Subalgebra.algebra_isAlgebraic_bot_left_iff, EssFiniteType.adjoin_mem_finset, adjoin_attach_biUnion, Polynomial.IsSplittingField.adjoin_rootSet, Subalgebra.prod_inf_prod, IntermediateField.inf_toSubalgebra, 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, 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, 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, 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, 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, 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, Subalgebra.bot_eq_top_of_finrank_eq_one, 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.restrictScalars_top, IsCentral.out, polynomialFunctions_closure_eq_top, IsDedekindDomain.integer_univ, IsAdjoinRoot.adjoin_root_eq_top, 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, 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	—
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 Finset.instMembership Finset.attach iSup Subalgebra SetLike.instMembership 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 📖	—	Set Set.instHasSubset SetLike.coe Subalgebra Subalgebra.instSetLike Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder adjoin	—	—	le_antisymm adjoin_le
adjoin_eq_ring_closure 📖	mathematical	—	Subalgebra.toSubring adjoin CommRing.toCommSemiring Ring.toSemiring Subring.closure 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 Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule adjoin	—	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	—	le_antisymm adjoin_le Subring.subset_closure Subring.closure_le subset_adjoin
adjoin_le 📖	mathematical	Set Set.instHasSubset SetLike.coe Subalgebra Subalgebra.instSetLike	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	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 📖	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin 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 📖	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet 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	—	—
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 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	Set.image 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	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	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra	—	le_sup_left
mem_sup_right 📖	mathematical	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	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 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 CommRing.toRing SetLike.instMembership Subring.instSetLike Subring.toCommRing 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.mem_carrier
toSubring_eq_top 📖	mathematical	—	Subalgebra.toSubring Top.top Subring 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 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	4 math math: mem_saturation_iff, Algebra.zariskisMainProperty_iff_exists_saturation_eq_top, saturation_saturation, le_saturation
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	Algebra.adjoin SetLike.coe instSetLike	—	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 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 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 SetLike.instMembership instSetLike saturation Submonoid.instSetLike Algebra.toSMul Algebra.id	—	—
mem_saturation_of_mul_mem_left 📖	—	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	—	—	Eq.le LE.le.trans le_saturation saturation_saturation
mem_saturation_of_mul_mem_right 📖	—	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	—	—	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 le_saturation	—	LE.le.antisymm' LE.le.trans le_saturation Submonoid.mul_mem mul_assoc
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 CommSemiring.toSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule Algebra.adjoin	—	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