| Metric | Count |
|---|
DefinitionsofInjective, ofInjectiveField, ofLeftInverse, subalgebraMap, codRestrict, equalizer, fintypeRange, range, rangeRestrict, subalgebraMap, toSubalgebra, algebra, algebra', center, centralizer, comap, copy, equivMapOfInjective, equivOfEq, inclusion, instCommRingSubtypeMemCenter, instCommSemiringSubtypeMemCenter, instDistribMulActionSubtypeMem, instInhabitedSubtypeMem, instModuleSubtypeMem, instMulActionSubtypeMem, instMulActionWithZeroSubtypeMem, instPartialOrder, instSMulSubtypeMem, instSMulWithZeroSubtypeMem, instSetLike, map, module', moduleLeft, ofClass, toAddSubmonoid, toAlgebra, toCommRing, toCommSemiring, toNonUnitalSubalgebra, toRing, toSemiring, toSubmodule, toSubmoduleEquiv, toSubring, toSubsemiring, val, toAlgebra, val, toSubalgebra, subalgebraOfSubring, subalgebraOfSubsemiring | 52 |
TheoremsofInjective_apply, ofLeftInverse_apply, ofLeftInverse_symm_apply, subalgebraMap_apply_coe, subalgebraMap_symm_apply_coe, coe_codRestrict, coe_equalizer, coe_range, equalizer_toSubmodule, equalizer_toSubsemiring, injective_codRestrict, le_equalizer, mem_equalizer, mem_range, mem_range_self, rangeRestrict_surjective, range_comp, range_comp_le_range, range_toSubsemiring, subalgebraMap_coe_apply, subalgebraMap_surjective, val_comp_codRestrict, val_comp_rangeRestrict, toSubalgebra_toNonUnitalSubalgebra, algebraMap_mem_center, algebraMap_mem_centralizer, add_mem, algebraMap_apply, algebraMap_def, algebraMap_eq, algebraMap_mem, algebraMap_mem', algebraMap_mk, center_le_centralizer, center_toSubring, center_toSubsemiring, centralizer_centralizer_centralizer, centralizer_le, centralizer_univ, coe_add, coe_algebraMap, coe_center, coe_centralizer, coe_comap, coe_copy, coe_eq_one, coe_eq_zero, coe_equivMapOfInjective_apply, coe_inclusion, coe_map, coe_mk, coe_mul, coe_neg, coe_ofClass, coe_one, coe_pow, coe_smul, coe_sub, coe_toAddSubmonoid, coe_toSubmodule, coe_toSubring, coe_toSubsemiring, coe_val, coe_zero, comap_map_eq_self_of_injective, comap_toSubsemiring, copy_eq, copy_toSubsemiring, equivOfEq_apply, equivOfEq_rfl, equivOfEq_symm, equivOfEq_trans, ext, ext_iff, gc_map_comap, faithfulSMul, isScalarTower_left, isScalarTower_right, inclusion_inclusion, inclusion_injective, inclusion_mk, inclusion_right, inclusion_self, instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMap, instFaithfulSMulSubtypeMem, instIsScalarTowerSubtypeMem, instIsTorsionFree, instIsTorsionFree', instSMulMemClass, instSubringClass, instSubsemiringClass, intCast_mem, isDomain, isScalarTower_left, isScalarTower_mid, isScalarTower_right, le_centralizer_centralizer, list_prod_mem, list_sum_mem, map_id, map_injective, map_le, map_map, map_mono, map_toSubmodule, map_toSubsemiring, mem_carrier, mem_center_iff, mem_centralizer_iff, mem_comap, mem_map, mem_mk, mem_toSubmodule, mem_toSubring, mem_toSubsemiring, mk_algebraMap, mul_mem, multiset_prod_mem, multiset_sum_mem, natCast_mem, neg_mem, noZeroDivisors, nsmul_mem, one_mem, one_mem_toNonUnitalSubalgebra, pow_mem, prod_mem, rangeS_algebraMap, rangeS_le, range_algebraMap, range_comp_val, range_le, range_subset, range_val, setRange_algebraMap, smulCommClass_left, smulCommClass_right, smul_def, smul_mem, sub_mem, subsingleton_of_subsingleton, sum_mem, toNonUnitalSubalgebra_toSubalgebra, toSubmodule_injective, toSubmodule_toSubalgebra, toSubring_inj, toSubring_injective, toSubring_subtype, toSubring_toSubsemiring, toSubsemiring_inj, toSubsemiring_injective, toSubsemiring_subtype, val_apply, val_comp_inclusion, zero_mem, zsmul_mem, coe_algebraMap, coe_val, coe_toSubalgebra, mem_toSubalgebra, toSubalgebra_mk, toSubalgebra_toSubmodule, toSubalgebra_toSubsemiring, algebraMap_mem, mem_subalgebraOfSubring, mem_subalgebraOfSubsemiring, subalgebraOfSubring_toSubsemiring, subalgebraOfSubsemiring_toSubsemiring | 168 |
| Total | 220 |
| Name | Category | Theorems |
|---|
algebra ๐ | CompOp | 245 mathmath: mulMap_comm, inclusion_right, minpoly.ToAdjoin.injective, centralizer_tensorProduct_eq_center_tensorProduct_right, Localization.subalgebra.isLocalization_subalgebra, StarAlgEquiv.ofInjective_symm_apply, AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm, Algebra.FiniteType.adjoin_of_finite, algebraicIndependent_adjoin, ValuationSubring.integralClosure_algebraMap_injective, AlgHom.val_comp_codRestrict, Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin, TensorProduct.toIntegralClosure_bijective_of_isLocalization, integralClosure.AlgebraIsIntegral, equivOfEq_apply, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, AlgHom.rangeRestrict_surjective, Algebra.IsIntegral.adjoin, Localization.isLocalization_range_mapToFractionRing, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, AlgHom.coe_mapIntegralClosure, AlgebraicIndependent.repr_ker, AlgEquiv.ofInjective_apply, centralizer_coe_map_includeLeft_eq_center_tensorProduct, MvPolynomial.supportedEquivMvPolynomial_symm_X, aeval_coe, Polynomial.lift_of_splits, mulMap_toLinearMap, RingCon.quotientKerEquivRangeโ_comp_mkโ, RingCon.coe_comapQuotientEquivRangeโ_mk, algebra_isAlgebraic_bot_right, val_apply, inclusion.isScalarTower_left, comm_trans_rTensorBot, mulMap_map_comp_eq, Algebra.EssFiniteType.adjoin_mem_finset, IsScalarTower.adjoin_range_toAlgHom, TensorProduct.toIntegralClosure_bijective_of_smooth, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, Algebra.TensorProduct.algEquivIncludeRange_symm_tmul, AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, AdjoinRoot.Minpoly.toAdjoin.surjective, AlgHom.val_comp_rangeRestrict, LinearDisjoint.linearIndependent_left_op_of_flat, AlgebraicIndependent.aeval_comp_repr, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, range_isScalarTower_toAlgHom, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, Field.Emb.Cardinal.succEquiv_coherence, AlgebraicGeometry.Scheme.Hom.ฮน_toNormalization, prod_mem_ideal_map_of_mem_conductor, Polynomial.aeval_subalgebra_coe, mopAlgEquivOp_symm_apply, inclusion_inclusion, LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply, TensorProduct.Algebra.exists_of_fg, centralizer_coe_image_includeRight_eq_center_tensorProduct, lTensorBot_one_tmul, Matrix.isRepresentation.toEnd_represents, mulMap_bot_left_eq, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, CliffordAlgebra.coe_toEven_reverse_involute, Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, AlgHom.coe_tensorEqualizer, isSeparable_iff, TensorProduct.toIntegralClosure_mvPolynomial_bijective, valA_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', ContinuousAlgHom.coe_codRestrict, Algebra.adjoin.powerBasis_dim, AlgHom.ker_rangeRestrict, mvPolynomial_aeval_coe, AdjoinRoot.Minpoly.coe_toAdjoin, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, CommRingCat.Under.tensorProdEqualizer_ฮน, topEquiv_apply, centralizer_coe_map_includeRight_eq_center_tensorProduct, isCyclotomicExtension_iff_eq_adjoin, range_val, AlgEquiv.ofLeftInverse_apply, MvPolynomial.rename_esymmAlgHom, CliffordAlgebra.even.lift_ฮน, mulMap'_surjective, coe_equivMapOfInjective_apply, Algebra.adjoin.powerBasis'_dim, LinearDisjoint.trace_algebraMap, Matrix.isRepresentation.toEnd_exists_mem_ideal, CliffordAlgebra.even.algHom_ext_iff, Submodule.lTensorOne'_tmul, Localization.subalgebra.isLocalization_ofField, AlgEquiv.coe_mapIntegralClosure, CliffordAlgebra.toEven_comp_ofEven, le_integralClosure_iff_isIntegral, Submodule.rTensorOne'_tmul, ContinuousAlgHom.coe_codRestrict_apply, MvPolynomial.esymmAlgHom_fin_surjective, NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe, quotAdjoinEquivQuotMap_apply_mk, LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, equivOfEq_rfl, fg_iff_finiteType, Submodule.rTensorOne_tmul, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient, inclusion_mk, inclusion_injective, Algebra.adjoin.powerBasis_gen, centralizer_tensorProduct_eq_center_tensorProduct_left, AlgebraicIndependent.algebraMap_aevalEquiv, AdjoinRoot.Minpoly.coe_toAdjoin_mk_X, rTensorBot_tmul_one, algebraMap_eq, AlgHom.tensorEqualizerEquiv_apply, ValuationSubring.isIntegral_of_mem_ringOfIntegers', CliffordAlgebra.evenToNeg_ฮน, inclusion.isScalarTower_right, RingCon.coe_comapQuotientEquivRangeโ_symm_mk, coe_val, mulMap_bot_right_eq, Algebra.TensorProduct.algEquivIncludeRange_tmul, Algebra.Smooth.exists_subalgebra_finiteType, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, LinearDisjoint.linearIndependent_right_of_flat, lTensorBot_symm_apply, coe_valA, inclusion_self, inclusion.faithfulSMul, RingCon.comapQuotientEquivRangeโ_mk, Submodule.range_valA, isCyclotomicExtension_singleton_iff_eq_adjoin, ValuationSubring.isIntegral_of_mem_ringOfIntegers, AlgebraicIndependent.aeval_repr, algEquivOpMop_apply, Algebra.adjoin_adjoin_coe_preimage, CliffordAlgebra.ofEven_comp_toEven, MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe, AlgEquiv.subalgebraMap_apply_coe, AlgebraicGeometry.Scheme.Hom.ฮน_toNormalization_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, Algebra.TensorProduct.algEquivIncludeRange_toAlgHom, Polynomial.coe_aeval_mk_apply, FunctionField.ringOfIntegers.algebraMap_injective, AlgHom.subalgebraMap_coe_apply, Algebra.essFiniteType_iff_exists_subalgebra, Submodule.exists_fg_of_baseChange_eq_zero, IsCyclotomicExtension.union_left, MvPolynomial.esymmAlgHom_fin_injective, CliffordAlgebra.even.lift_symm_apply_bilin, CliffordAlgebra.evenEquivEvenNeg_apply, linearDisjoint_iff_injective, fg_top, Ideal.IntegralClosure.comap_lt_comap, CliffordAlgebra.toEven_ฮน, Algebra.restrictScalars_adjoin, lTensorBot_tmul, topEquiv_symm_apply_coe, Algebra.isIntegral_iSup, TensorProduct.toIntegralClosure_injective_of_flat, isAlgebraic_iff_isAlgebraic_val, Algebra.isIntegral_sup, Matrix.isRepresentation.toEnd_surjective, Algebra.adjoin_restrictScalars, AlgEquiv.ofLeftInverse_symm_apply, LinearDisjoint.val_mulMap_tmul, minpoly.equivAdjoin_toAlgHom, RingCon.quotientKerEquivRangeโ_mkโ, MvPolynomial.esymmAlgHom_apply, mulMap_range, centralizer_coe_range_includeLeft_eq_center_tensorProduct, AlgebraicIndependent.aevalEquiv_apply_coe, rTensorBot_symm_apply, AlgHom.subalgebraMap_surjective, LinearDisjoint.mulMapLeftOfSupEqTop_tmul, range_comp_val, Matrix.isRepresentation.eq_toEnd_of_represents, Algebra.mem_ideal_map_adjoin, LinearDisjoint.linearIndependent_left_of_flat_of_commute, minpoly.coe_equivAdjoin, Algebra.adjoin.powerBasis'_minpoly_gen, Algebra.instFiniteTypeSubtypeMemSubalgebraSubalgebra, ContinuousAlgHom.coe_rangeRestrict, CliffordAlgebra.even.lift.aux_ฮน, CommRingCat.Under.equalizerFork_ฮน, IsLocalization.integralClosure, Algebra.TensorProduct.algEquivIncludeRange_symm_toAlgHom, Submodule.lTensorOne_tmul, comm_trans_lTensorBot, CliffordAlgebra.evenEquivEvenNeg_symm_apply, ContinuousMap.polynomial_comp_attachBound, IsPrimitiveRoot.adjoin_isCyclotomicExtension, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, CliffordAlgebra.ofEven_ฮน, instSMulCommClassSubtypeMemSubalgebraIntegralClosure, toSubring_subtype, integralClosure.isIntegral, val_comp_inclusion, LinearDisjoint.linearIndependent_left_of_flat, centralizer_coe_image_includeLeft_eq_center_tensorProduct, IsScalarTower.subalgebra', MvPolynomial.esymmAlgHom_fin_bijective, AlgHom.coe_codRestrict, instFiniteTypeSubtypePolynomialMemSubalgebraReesAlgebraOfIsNoetherianRing, MvPolynomial.esymmAlgEquiv_apply, val_mulMap'_tmul, LinearDisjoint.norm_algebraMap, isAlgebraic_iff, Algebra.adjoin_union_eq_adjoin_adjoin, Algebra.adjoin.powerBasis'_gen, LinearDisjoint.isDomain, AlgHom.injective_codRestrict, toSubsemiring_subtype, equivOfEq_symm, isIntegral_iff, LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, mulMap_tmul, AlgEquiv.subalgebraMap_symm_apply_coe, MvPolynomial.supportedEquivMvPolynomial_symm_C, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, CliffordAlgebra.evenToNeg_comp_evenToNeg, mopAlgEquivOp_apply_coe, instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure, IsLocalization.Away.integralClosure, LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, algEquivOpMop_symm_apply_coe, rTensorBot_tmul, instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra, mk_algebraMap, IsCyclotomicExtension.lcm_sup, coe_valA', AlgebraicGeometry.Scheme.Hom.fromNormalization_app, Algebra.botEquiv_symm_apply, RingCon.coe_quotientKerEquivRangeโ_mkโ, Algebra.TensorProduct.linearEquivIncludeRange_tmul, MvPolynomial.esymmAlgHom_surjective, CommRingCat.Under.equalizer_comp, centralizer_range_includeRight_eq_center_tensorProduct, MvPolynomial.esymmAlgEquiv_symm_apply, equivOfEq_trans, CommRingCat.Under.equalizerFork'_ฮน, coe_inclusion, MvPolynomial.esymmAlgHom_injective, comap_map_eq_map_adjoin_of_coprime_conductor, MvPolynomial.renameSymmetricSubalgebra_apply_coe, CliffordAlgebra.even.lift.aux_algebraMap, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
|
algebra' ๐ | CompOp | 2 mathmath: coe_algebraMap, IntermediateField.isAlgebraic_adjoin_iff_bot
|
center ๐ | CompOp | 19 mathmath: centralizer_tensorProduct_eq_center_tensorProduct_right, Algebra.TensorProduct.includeLeft_map_center_le, center_toSubsemiring, coe_center, mem_center_iff, center_eq_top, Algebra.TensorProduct.includeRight_map_center_le, centralizer_tensorProduct_eq_center_tensorProduct_left, centralizer_eq_top_iff_subset, Algebra.IsCentral.mem_center_iff, center_le_centralizer, centralizer_coe_range_includeLeft_eq_center_tensorProduct, Algebra.IsCentral.center_eq_bot, Matrix.subalgebraCenter_eq_scalarAlgHom_map, center_toSubring, centralizer_univ, Algebra.IsCentral.out, Module.End.mem_subalgebraCenter_iff, centralizer_range_includeRight_eq_center_tensorProduct
|
centralizer ๐ | CompOp | 23 mathmath: centralizer_tensorProduct_eq_center_tensorProduct_right, centralizer_coe_map_includeLeft_eq_center_tensorProduct, centralizer_coe_iSup, le_centralizer_iff, centralizer_coe_image_includeRight_eq_center_tensorProduct, Algebra.elemental.le_centralizer_centralizer, le_centralizer_centralizer, centralizer_coe_map_includeRight_eq_center_tensorProduct, StarSubalgebra.centralizer_toSubalgebra, centralizer_centralizer_centralizer, centralizer_tensorProduct_eq_center_tensorProduct_left, centralizer_eq_top_iff_subset, centralizer_le, Algebra.adjoin_le_centralizer_centralizer, center_le_centralizer, centralizer_coe_range_includeLeft_eq_center_tensorProduct, centralizer_coe_sup, centralizer_coe_image_includeLeft_eq_center_tensorProduct, centralizer_univ, coe_centralizer, topologicalClosure_adjoin_le_centralizer_centralizer, centralizer_range_includeRight_eq_center_tensorProduct, mem_centralizer_iff
|
comap ๐ | CompOp | 16 mathmath: comap_map_eq, comap_map_eq_self_of_injective, map_comap_eq_self, gc_map_comap, map_le, comap_toSubsemiring, mem_comap, map_comap_eq_self_of_surjective, coe_comap, Algebra.comap_top, map_comap_eq, comap_map_eq_self, topologicalClosure_comap_homeomorph, SeparatesPoints.rclike_to_real, RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict, polynomialFunctions.comap_compRightAlgHom_iccHomeoI
|
copy ๐ | CompOp | 3 mathmath: copy_eq, copy_toSubsemiring, coe_copy
|
equivMapOfInjective ๐ | CompOp | 1 mathmath: coe_equivMapOfInjective_apply
|
equivOfEq ๐ | CompOp | 4 mathmath: equivOfEq_apply, equivOfEq_rfl, equivOfEq_symm, equivOfEq_trans
|
inclusion ๐ | CompOp | 13 mathmath: inclusion_right, inclusion.isScalarTower_left, Field.Emb.Cardinal.succEquiv_coherence, inclusion_inclusion, TensorProduct.Algebra.eq_of_fg_of_subtype_eq, inclusion_mk, inclusion_injective, TensorProduct.Algebra.eq_of_fg_of_subtype_eq', inclusion.isScalarTower_right, inclusion_self, inclusion.faithfulSMul, val_comp_inclusion, coe_inclusion
|
instCommRingSubtypeMemCenter ๐ | CompOp | โ |
instCommSemiringSubtypeMemCenter ๐ | CompOp | โ |
instDistribMulActionSubtypeMem ๐ | CompOp | โ |
instInhabitedSubtypeMem ๐ | CompOp | โ |
instModuleSubtypeMem ๐ | CompOp | 104 mathmath: mulMap_comm, Submodule.rTensorOne_symm_apply, adjoin_rank_le, Submodule.comm_trans_lTensorOne, LinearDisjoint.sup_free_of_free, CliffordAlgebra.even.lift.aux_mul, Algebra.finite_adjoin_simple_of_isIntegral, Submodule.mulMap_one_right_eq, finrank_sup_eq_finrank_right_mul_finrank_of_free, TensorProduct.toIntegralClosure_bijective_of_isLocalization, rank_sup_eq_rank_left_mul_rank_of_free, LinearDisjoint.adjoin_rank_eq_rank_left, mulMap_toLinearMap, mulMap_map_comp_eq, TensorProduct.toIntegralClosure_bijective_of_smooth, Algebra.TensorProduct.algEquivIncludeRange_symm_tmul, Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap, range_isScalarTower_toAlgHom, LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply, instIsTorsionFree, LinearDisjoint.rank_sup_of_free, finrank_toSubmodule, lTensorBot_one_tmul, mulMap_bot_left_eq, AlgHom.coe_tensorEqualizer, TensorProduct.toIntegralClosure_mvPolynomial_bijective, finrank_right_dvd_finrank_sup_of_free, FiniteDimensional.of_subalgebra_toSubmodule, isNoetherian_adjoin_finset, linearEquivOp_apply_coe, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, mulMap'_surjective, Submodule.comm_trans_rTensorOne, adjoin_eq_span_basis, LinearDisjoint.algebraMap_basisOfBasisRight_apply, finrank_left_dvd_finrank_sup_of_free, Submodule.lTensorOne'_tmul, Submodule.rTensorOne'_tmul_one, Submodule.rTensorOne'_tmul, IntermediateField.finrank_eq_finrank_subalgebra, Submodule.rTensorOne_tmul, rTensorBot_tmul_one, LinearDisjoint.rank_eq_one_of_commute_of_flat_of_self_of_inj, AlgHom.tensorEqualizerEquiv_apply, Algebra.finite_adjoin_of_finite_of_isIntegral, finrank_sup_eq_finrank_left_mul_finrank_of_free, finrank_sup_le_of_free, Submodule.rTensorOne_tmul_one, finite_sup, mulMap_bot_right_eq, Algebra.TensorProduct.linearEquivIncludeRange_symm_tmul, Algebra.TensorProduct.algEquivIncludeRange_tmul, rank_sup_eq_rank_right_mul_rank_of_free, lTensorBot_symm_apply, finiteDimensional_toSubmodule, Submodule.mulMap_one_left_eq, LinearDisjoint.rank_inf_eq_one_of_flat_left_of_inj, FiniteDimensional.finiteDimensional_subalgebra, LinearDisjoint.finrank_sup_of_free, Algebra.TensorProduct.algEquivIncludeRange_toAlgHom, linearDisjoint_iff_injective, lTensorBot_tmul, rank_sup_le_of_free, TensorProduct.toIntegralClosure_injective_of_flat, LinearDisjoint.val_mulMap_tmul, mulMap_range, LinearDisjoint.basisOfBasisLeft_apply, rTensorBot_symm_apply, LinearDisjoint.mulMapLeftOfSupEqTop_tmul, LinearDisjoint.rank_inf_eq_one_of_flat_right_of_inj, Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap, Submodule.lTensorOne_symm_apply, instIsScalarTowerSubtypeMem, Submodule.lTensorOne'_one_tmul, CliffordAlgebra.even.lift.aux_apply, CliffordAlgebra.even.lift.aux_ฮน, rank_eq_one_iff, FunctionField.ringOfIntegers.instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc, subalgebra_top_finrank_eq_submodule_top_finrank, linearEquivOp_symm_apply_coe, Algebra.TensorProduct.algEquivIncludeRange_symm_toAlgHom, Submodule.lTensorOne_tmul, LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_left_of_inj, IntermediateField.rank_eq_rank_subalgebra, val_mulMap'_tmul, LinearDisjoint.isDomain, Submodule.lTensorOne_one_tmul, mulMap_tmul, finrank_bot, LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_right_of_inj, LinearDisjoint.adjoin_rank_eq_rank_right, LinearDisjoint.basisOfBasisLeft_repr_apply, rTensorBot_tmul, LinearDisjoint.rank_eq_one_of_flat_of_self_of_inj, rank_bot, rank_toSubmodule, rank_top, Algebra.TensorProduct.linearEquivIncludeRange_tmul, finrank_eq_one_iff, subalgebra_top_rank_eq_submodule_top_rank, CliffordAlgebra.even.lift.aux_one, finite_bot, Algebra.rank_adjoin_le, CliffordAlgebra.even.lift.aux_algebraMap
|
instMulActionSubtypeMem ๐ | CompOp | โ |
instMulActionWithZeroSubtypeMem ๐ | CompOp | โ |
instPartialOrder ๐ | CompOp | 119 mathmath: integralClosure_le_span_dualBasis, toSubmodule_injective, Algebra.TensorProduct.includeLeft_map_center_le, mem_subalgebraEquivIntermediateField, integralClosure_le_completeIntegralClosure, Submodule.mulMap_one_right_eq, adjoin_le_integralClosure, UnitAddTorus.mFourierSubalgebra_coe, polynomialFunctions.le_equalizer, mulMap_toLinearMap, Algebra.elemental.le_iff_mem, AlgHom.le_equalizer, Submonoid.adjoin_eq_span_of_eq_span, Algebra.span_le_adjoin, AlgHom.range_comp_le_range, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, mem_toSubmodule, range_isScalarTower_toAlgHom, Algebra.toSubmodule_bot, Algebra.sInf_toSubmodule, le_centralizer_iff, finrank_toSubmodule, isIdempotentElem_toSubmodule, Algebra.TensorProduct.includeRight_map_center_le, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, isSimpleOrder_of_finrank, span_coeff_minpolyDiv, separatesPoints_monotone, Algebra.top_toSubmodule, Algebra.elemental.le_centralizer_centralizer, integralClosure_le_algebraicClosure, mem_subalgebraEquivIntermediateField_symm, instCovariantClassHSMulLe, Algebra.adjoin_singleton_le, Submodule.toSubalgebra_toSubmodule, le_centralizer_centralizer, traceForm_dualSubmodule_adjoin, FractionalIdeal.adjoinIntegral_coe, mul_toSubmodule, Algebra.adjoin_nonUnitalSubalgebra_eq_span, gc_map_comap, FractionalIdeal.isFractional_adjoin_integral, mem_integralClosure_iff_mem_fg, adjoin_eq_span_basis, le_integralClosure_iff_isIntegral, topologicalClosure_map_le, mul_toSubmodule_le, unop_le_unop_iff, Module.Flat.instSubalgebraToSubmodule, Algebra.adjoin_toSubmodule_le, MvPolynomial.supported_strictMono, LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, starClosure_le_iff, MvPolynomial.supported_mono, Algebra.inf_toSubmodule, Algebra.adjoin_eq_span_of_subset, linearDisjoint_iff, map_le, map_toSubmodule, Submodule.span_range_natDegree_eq_adjoin, centralizer_le, op_le_iff, Algebra.iInf_toSubmodule, fourierSubalgebra_coe, inclusion_self, finiteDimensional_toSubmodule, toSubmodule_toSubalgebra, StarSubalgebra.toSubalgebra_le_iff, Algebra.adjoin_union_coe_submodule, Submodule.mulMap_one_left_eq, le_topologicalClosure, fg_adjoin_of_finite, IsCyclotomicExtension.le_of_dvd, Algebra.adjoin_le_centralizer_centralizer, Algebra.adjoin_eq_span, CliffordAlgebra.even_toSubmodule, Algebra.toSubmodule_eq_top, center_le_centralizer, pi_toSubsemiring, Algebra.adjoin_mono, Algebra.adjoin_le_iff, MvPolynomial.supported_le_supported_iff, Algebra.adjoin_prod_le, AlgHom.adjoin_le_equalizer, map_topologicalClosure_le, coe_pi, Algebra.adjoin_le, le_saturation, coe_toSubmodule, IntermediateField.toSubalgebra_lt_toSubalgebra, opEquiv_symm_apply, Unitization.lift_range_le, restrictScalars_toSubmodule, StarAlgebra.adjoin_eq_span, Submodule.iSup_eq_toSubmodule_range, isSimpleOrder_of_finrank_prime, IntermediateField.toSubalgebra_strictMono, IsIntegral.fg_adjoin_singleton, MvPolynomial.range_mapAlgHom, IntermediateField.le_sup_toSubalgebra, FiniteDimensional.subalgebra_toSubmodule, IntermediateField.toSubalgebra_le_toSubalgebra, pointwise_smul_toSubmodule, prod_toSubmodule, le_op_iff, Algebra.elemental.le_of_mem, Algebra.IsCentral.out, star_mono, LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, AlgHom.equalizer_toSubmodule, pi_toSubmodule, op_le_op_iff, topologicalClosure_adjoin_le_centralizer_centralizer, Algebra.gc, rank_toSubmodule, fg_bot_toSubmodule, opEquiv_apply, IntermediateField.algebra_adjoin_le_adjoin, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
|
instSMulSubtypeMem ๐ | CompOp | 14 mathmath: instSMulDistribClassSubtypeMemSubalgebraIntegralClosure, Algebra.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap, smulCommClass_right, IsScalarTower.subalgebra, isScalarTower_left, instFaithfulSMulSubtypeMem, isScalarTower_mid, smulCommClass_left, minpoly.instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure, continuousSMul, IsScalarTower.subalgebra', smul_def, IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1, IntermediateField.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap
|
instSMulWithZeroSubtypeMem ๐ | CompOp | โ |
instSetLike ๐ | CompOp | 634 mathmath: IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime, mem_restrictScalars, Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, exists_fg_and_mem_baseChange, StarSubalgebra.mem_toSubalgebra, mulMap_comm, AlgHom.mem_range_self, Submodule.rTensorOne_symm_apply, minpoly.ToAdjoin.injective, Algebra.RingHom.adjoin_algebraMap_apply, Ideal.Filtration.submodule_closure_single, centralizer_tensorProduct_eq_center_tensorProduct_right, Localization.subalgebra.isLocalization_subalgebra, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, Algebra.lift_cardinalMk_adjoin_le, StarAlgEquiv.ofInjective_symm_apply, Polynomial.mem_lifts_iff_mem_alg, adjoin_rank_le, AlgebraicIndependent.transcendental_adjoin_iff, AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm, Algebra.mem_iInf, coe_iSup_of_directed, Algebra.FiniteType.adjoin_of_finite, algebraicIndependent_adjoin, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow, ContinuousMap.abs_mem_subalgebra_closure, ValuationSubring.integralClosure_algebraMap_injective, IsCyclotomicExtension.mem_of_pow_eq_one, Submodule.comm_trans_lTensorOne, spinGroup.mem_even, mem_op, Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin, mem_reesAlgebra_iff_support, LinearDisjoint.sup_free_of_free, mem_subalgebraEquivIntermediateField, AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic, jacobiSum_mem_algebraAdjoin_of_pow_eq_one, Algebra.mem_top, CliffordAlgebra.even.lift.aux_mul, Algebra.finite_adjoin_simple_of_isIntegral, MulChar.apply_mem_algebraAdjoin_of_pow_eq_one, Submodule.mulMap_one_right_eq, Localization.isFractionRing_range_mapToFractionRing, finrank_sup_eq_finrank_right_mul_finrank_of_free, TensorProduct.toIntegralClosure_bijective_of_isLocalization, integralClosure.AlgebraIsIntegral, equivOfEq_apply, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, AlgebraicIndependent.transcendental_adjoin, AlgHom.rangeRestrict_surjective, mem_algebraicClosure, Algebra.IsIntegral.adjoin, topologicalClosure_coe, Localization.isLocalization_range_mapToFractionRing, coe_center, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, AlgHom.coe_mapIntegralClosure, Algebra.sSup_def, AlgebraicIndependent.repr_ker, Set.unitEquivUnitsInteger_symm_apply_coe, ContinuousMap.continuousMap_mem_subalgebra_closure_of_separatesPoints, AlgEquiv.ofInjective_apply, centralizer_coe_map_includeLeft_eq_center_tensorProduct, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, Algebra.mem_sInf, integralClosure.isIntegrallyClosedOfFiniteExtension, SeparatesPoints.strongly, centralizer_coe_iSup, rank_sup_eq_rank_left_mul_rank_of_free, mem_center_iff, IsPrimitiveRoot.subOneIntegralPowerBasis_gen, AlgebraicIndependent.iff_adjoin_image_compl, MulChar.apply_mem_algebraAdjoin, coe_one, MvPolynomial.supportedEquivMvPolynomial_symm_X, Submodule.coe_toSubalgebra, aeval_coe, LinearDisjoint.adjoin_rank_eq_rank_left, Polynomial.lift_of_splits, mulMap_toLinearMap, Ideal.Filtration.mem_submodule, Algebra.mem_adjoin_iff, Algebra.elemental.le_iff_mem, AlgHom.le_equalizer, instIsTorsionFree', MonoidAlgebra.mem_adjoin_support, RingCon.quotientKerEquivRangeโ_comp_mkโ, IntermediateField.algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin, coe_pointwise_smul, RingCon.coe_comapQuotientEquivRangeโ_mk, algebra_isAlgebraic_bot_right, FunctionField.ringOfIntegers.instIsIntegralClosureSubtypeMemSubalgebraPolynomial, val_apply, AlgebraicIndependent.matroid_isBasis_iff, AlgHom.coe_range, inclusion.isScalarTower_left, mem_subalgebraOfSubsemiring, comm_trans_rTensorBot, mulMap_map_comp_eq, algebra_isAlgebraic_bot_left_iff, Algebra.elemental.isClosedEmbedding_coe, Algebra.EssFiniteType.adjoin_mem_finset, IsScalarTower.adjoin_range_toAlgHom, TensorProduct.toIntegralClosure_bijective_of_smooth, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, spinGroup.mem_iff, IntermediateField.isAlgebraic_adjoin_iff_top, Algebra.TensorProduct.algEquivIncludeRange_symm_tmul, AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, AdjoinRoot.Minpoly.toAdjoin.surjective, AlgHom.val_comp_rangeRestrict, AlgebraicIndependent.aeval_comp_repr, integralClosure_idem, Algebra.adjoin_adjoin_of_tower, AlgebraicIndependent.adjoin_iff_disjoint, Algebra.mem_bot, Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap, IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_one, Algebra.coe_iInf, IntermediateField.isAlgebraic_adjoin_iff, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, mem_toSubmodule, Localization.subalgebra.mem_range_mapToFractionRing_iff_ofField, AlgebraicIndependent.matroid_spanning_iff, zero_mem, range_isScalarTower_toAlgHom, coe_sub, integralClosure.isDedekindDomain, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, instSMulDistribClassSubtypeMemSubalgebraIntegralClosure, IntermediateField.coe_toSubalgebra, Field.Emb.Cardinal.succEquiv_coherence, AlgebraicGeometry.Scheme.Hom.ฮน_toNormalization, prod_mem_ideal_map_of_mem_conductor, mem_adjoin_map_integralClosure_of_isStandardEtale, Polynomial.aeval_subalgebra_coe, Algebra.coe_bot, mopAlgEquivOp_symm_apply, inclusion_inclusion, monomial_mem_adjoin_monomial, Algebra.elemental.instCompleteSpaceSubtypeMemSubalgebra, Algebra.subset_adjoin, LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime, TensorProduct.Algebra.exists_of_fg, continuousMap_mem_polynomialFunctions_closure, FunctionField.classNumber_eq_one_iff, le_centralizer_iff, coe_mul, centralizer_coe_image_includeRight_eq_center_tensorProduct, instIsTorsionFree, MvPolynomial.transcendental_supported_X_iff, LinearDisjoint.rank_sup_of_free, finrank_toSubmodule, algebraMap_def, Algebra.coe_top, AlgebraicIndependent.sumElim_iff, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime, lTensorBot_one_tmul, Matrix.isRepresentation.toEnd_represents, mulMap_bot_left_eq, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, isScalarTower_right, CliffordAlgebra.coe_toEven_reverse_involute, Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, coe_op, integralClosure.isFractionRing_of_finite_extension, AlgHom.coe_tensorEqualizer, isSeparable_iff, TensorProduct.toIntegralClosure_mvPolynomial_bijective, AlgebraicIndependent.adjoin_of_disjoint, valA_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', Algebra.essFiniteType_cond_iff, Algebra.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap, Algebra.elemental.le_centralizer_centralizer, IsFractionRing.algHom_fieldRange_eq_of_comp_eq, Set.coe_integer, Algebra.Presentation.coeffs_subset_core, mem_subalgebraEquivIntermediateField_symm, Algebra.adjoin.powerBasis_dim, Algebra.Presentation.coeffs_relation_subset_core, AlgHom.ker_rangeRestrict, mvPolynomial_aeval_coe, mem_starClosure, AdjoinRoot.Minpoly.coe_toAdjoin, le_centralizer_centralizer, mem_conductor_iff, finrank_right_dvd_finrank_sup_of_free, FiniteDimensional.of_subalgebra_toSubmodule, IsIntegral.mem_range_algHom_of_minpoly_splits, AlgebraicIndependent.subalgebraAlgebraicClosure, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, isNoetherian_adjoin_finset, ContinuousMap.sup_mem_closed_subalgebra, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen, mem_completeIntegralClosure, FunctionField.ringOfIntegers.instIsDomainSubtypeMemSubalgebraPolynomial, linearEquivOp_apply_coe, roots_mem_integralClosure, CommRingCat.Under.tensorProdEqualizer_ฮน, topEquiv_apply, mem_carrier, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, NumberField.house.exists_ne_zero_int_vec_house_le, centralizer_coe_map_includeRight_eq_center_tensorProduct, mem_saturation_iff, isCyclotomicExtension_iff_eq_adjoin, AlgHom.mem_range, range_val, AlgEquiv.ofLeftInverse_apply, MvPolynomial.mem_supported, MvPolynomial.rename_esymmAlgHom, mem_integralClosure_iff_mem_fg, CliffordAlgebra.even.lift_ฮน, coeff_minpolyDiv_mem_adjoin, mem_subalgebraOfSubring, ContinuousMap.exists_mem_subalgebra_near_continuousMap_of_separatesPoints, mulMap'_surjective, Submodule.comm_trans_rTensorOne, coe_equivMapOfInjective_apply, mem_map, adjoin_eq_span_basis, isField_of_algebraic, LinearDisjoint.algebraMap_basisOfBasisRight_apply, FunctionField.ringOfIntegers.instIsIntegrallyClosedSubtypeMemSubalgebraPolynomial, Algebra.adjoin.powerBasis'_dim, LinearDisjoint.trace_algebraMap, AlgebraicIndependent.isAlgebraic_adjoin_iff_of_matroid_isBasis, Matrix.isRepresentation.toEnd_exists_mem_ideal, instIsNoetherianRingSubtypePolynomialMemSubalgebraReesAlgebra, coe_algebraMap, IntermediateField.mem_adjoin_iff_div, CliffordAlgebra.even.algHom_ext_iff, finrank_left_dvd_finrank_sup_of_free, Submodule.lTensorOne'_tmul, Localization.subalgebra.isLocalization_ofField, Submodule.rTensorOne'_tmul_one, AlgEquiv.coe_mapIntegralClosure, CliffordAlgebra.toEven_comp_ofEven, le_integralClosure_iff_isIntegral, reesAlgebra.monomial_mem, Ideal.Filtration.inf_submodule, Submodule.rTensorOne'_tmul, MvPolynomial.esymmAlgHom_fin_surjective, integralClosure.isNoetherianRing, IntermediateField.finrank_eq_finrank_subalgebra, smulCommClass_right, ContinuousAlgHom.eqOn_closure_adjoin, ContinuousMap.sup_mem_subalgebra_closure, conductor_subset_adjoin, exists_jacobiSum_eq_neg_one_add, Derivation.eqOn_adjoin, starClosure_eq_adjoin, Algebra.Presentation.instHasCoeffsSubtypeMemSubalgebraAdjoin, NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, Set.val_unitEquivUnitsInteger_apply_coe, LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, ContinuousMap.inf_mem_subalgebra_closure, IsScalarTower.subalgebra, equivOfEq_rfl, ContinuousMap.inf_mem_closed_subalgebra, Ideal.Filtration.submodule_span_single, Algebra.EssFiniteType.isLocalization, fg_iff_finiteType, Submodule.rTensorOne_tmul, isScalarTower_left, ContinuousMap.exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints, intCast_mem, Algebra.elemental.self_mem, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient, toIsStrictOrderedRing, noZeroDivisors, inclusion_injective, Algebra.adjoin.powerBasis_gen, NumberField.RingOfIntegers.mk_zero, coe_matrix, coe_star, MvPolynomial.mem_supported_vars, AlgebraicIndependent.option_iff_transcendental, mem_mk, centralizer_tensorProduct_eq_center_tensorProduct_left, Algebra.discr_mul_isIntegral_mem_adjoin, Ideal.IntegralClosure.isMaximal_of_isMaximal_comap, coe_restrictScalars, AlgebraicIndependent.algebraMap_aevalEquiv, AdjoinRoot.Minpoly.coe_toAdjoin_mk_X, IsCyclotomicExtension.iff_singleton, centralizer_eq_top_iff_subset, rTensorBot_tmul_one, MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero, algebraMap_eq, instIsIntegrallyClosedInSubtypeMemSubalgebraIntegralClosure, exists_subalgebra_of_fg, AlgHom.tensorEqualizerEquiv_apply, mem_integralClosure_iff, Algebra.finite_adjoin_of_finite_of_isIntegral, finrank_sup_eq_finrank_left_mul_finrank_of_free, Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree, Algebra.adjoin_insert_adjoin, finrank_sup_le_of_free, ValuationSubring.isIntegral_of_mem_ringOfIntegers', coe_ofClass, mem_unop, IntermediateField.isTranscendenceBasis_adjoin_iff, CliffordAlgebra.evenToNeg_ฮน, Submodule.rTensorOne_tmul_one, coe_toSubsemiring, integralClosure.isFractionRing_of_algebraic, Algebra.small_adjoin, Ring.DimensionLEOne.integralClosure, inclusion.isScalarTower_right, Algebra.adjoin_eq_exists_aeval, coe_smul, instFaithfulSMulSubtypeMem, AlgebraicIndepOn.insert_iff, RingCon.coe_comapQuotientEquivRangeโ_symm_mk, finite_sup, coe_eq_one, coe_val, mulMap_bot_right_eq, Algebra.TensorProduct.linearEquivIncludeRange_symm_tmul, Algebra.TensorProduct.algEquivIncludeRange_tmul, Algebra.Smooth.exists_subalgebra_finiteType, coe_map, rank_sup_eq_rank_right_mul_rank_of_free, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, lTensorBot_symm_apply, Module.End.exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow, Algebra.Etale.exists_subalgebra_fg, coe_valA, inclusion_self, inclusion.faithfulSMul, finiteDimensional_toSubmodule, NumberField.RingOfIntegers.mk_one, isScalarTower_mid, RingCon.comapQuotientEquivRangeโ_mk, Submodule.range_valA, StarSubalgebra.coe_mk, isAlgebraic_iff_exists_isTranscendenceBasis_subset, FunctionField.ringOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc, isCyclotomicExtension_singleton_iff_eq_adjoin, Submodule.mulMap_one_left_eq, AlgebraicIndependent.aeval_repr, algEquivOpMop_apply, coe_neg, instIsTopologicalSemiringSubtypeMemSubalgebra, Algebra.IsCentral.mem_center_iff, AlgHom.eqOn_adjoin_iff, Algebra.adjoin_adjoin_coe_preimage, LinearDisjoint.rank_inf_eq_one_of_flat_left_of_inj, CliffordAlgebra.ofEven_comp_toEven, minpoly.ofSubring, Algebra.adjoin_top, instSMulMemClass, MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe, Algebra.adjoin_le_centralizer_centralizer, AlgEquiv.subalgebraMap_apply_coe, FiniteDimensional.finiteDimensional_subalgebra, AlgebraicGeometry.Scheme.Hom.ฮน_toNormalization_assoc, LinearDisjoint.finrank_sup_of_free, Algebra.mem_adjoin_of_mem, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, mem_comap, Algebra.TensorProduct.algEquivIncludeRange_toAlgHom, Localization.subalgebra.isFractionRing, FunctionField.ringOfIntegers.algebraMap_injective, AlgHom.subalgebraMap_coe_apply, AddMonoidAlgebra.mem_adjoin_support, Algebra.essFiniteType_iff_exists_subalgebra, Submodule.exists_fg_of_baseChange_eq_zero, coe_zero, IsCyclotomicExtension.union_left, MvPolynomial.X_mem_supported, MvPolynomial.esymmAlgHom_fin_injective, IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin, Algebra.adjoin_le_iff, polynomialFunctions_coe, CliffordAlgebra.even.lift_symm_apply_bilin, CliffordAlgebra.evenEquivEvenNeg_apply, linearDisjoint_iff_injective, fg_top, mem_toSubsemiring, Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le, CliffordAlgebra.toEven_ฮน, IntermediateField.mem_toSubalgebra, smulCommClass_left, instSubringClass, Algebra.restrictScalars_adjoin, integralClosure.coe_smul, IntermediateField.topEquiv_symm_apply_coe, Transcendental.subalgebraAlgebraicClosure, lTensorBot_tmul, AlgCat.instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra, topEquiv_symm_apply_coe, coe_comap, star_mem_star_iff, Algebra.isIntegral_iSup, rank_sup_le_of_free, TensorProduct.toIntegralClosure_injective_of_flat, isAlgebraic_iff_isAlgebraic_val, rangeS_algebraMap, IntermediateField.topEquiv_apply, Algebra.isIntegral_sup, Matrix.isRepresentation.toEnd_surjective, coe_pi, Localization.subalgebra.isFractionRing_ofField, FunctionField.ringOfIntegers.instIsFractionRingSubtypeMemSubalgebraPolynomial, ContinuousMap.comp_attachBound_mem_closure, Algebra.adjoin_restrictScalars, mem_coeSubmodule_conductor, isCyclotomicExtension_iff, AlgEquiv.ofLeftInverse_symm_apply, range_subset, LinearDisjoint.val_mulMap_tmul, minpoly.equivAdjoin_toAlgHom, RingCon.quotientKerEquivRangeโ_mkโ, MvPolynomial.esymmAlgHom_apply, mulMap_range, LinearDisjoint.basisOfBasisLeft_apply, MvPolynomial.irreducible_toPolynomialAdjoinImageCompl, Algebra.elemental.isClosed, centralizer_coe_range_includeLeft_eq_center_tensorProduct, AlgebraicIndependent.aevalEquiv_apply_coe, rTensorBot_symm_apply, AlgHom.subalgebraMap_surjective, LinearDisjoint.mulMapLeftOfSupEqTop_tmul, LinearDisjoint.rank_inf_eq_one_of_flat_right_of_inj, Algebra.RingHom.adjoin_algebraMap_surjective, adjoin_eq_span_of_eq_span, IsAlgebraic.exists_nonzero_eq_adjoin_mul, instSubsemiringClass, Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap, range_comp_val, centralizer_coe_sup, Submodule.lTensorOne_symm_apply, coe_eq_zero, coe_starClosure, AlgebraicIndependent.option_iff, IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin, Algebra.mem_ideal_map_adjoin, coe_unop, instIsScalarTowerSubtypeMem, Algebra.adjoin_eq, JacobsonNoether.exists_separable_and_not_isCentral', IsPowMul.restriction, Submodule.lTensorOne'_one_tmul, AlgebraicIndependent.matroid_closure_eq, minpoly.coe_equivAdjoin, AlgebraicIndependent.integralClosure, Algebra.adjoin.powerBasis'_minpoly_gen, Algebra.instFiniteTypeSubtypeMemSubalgebraSubalgebra, ContinuousAlgHom.coe_rangeRestrict, toIsOrderedRing, CliffordAlgebra.even.lift.aux_apply, CliffordAlgebra.even.lift.aux_ฮน, Algebra.eq_top_iff, rank_eq_one_iff, mem_reesAlgebra_iff, FunctionField.ringOfIntegers.instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, coe_toSubmodule, FG.small, subalgebra_top_finrank_eq_submodule_top_finrank, CommRingCat.Under.equalizerFork_ฮน, IsLocalization.integralClosure, Algebra.adjoin_eq_sInf, AlgebraicIndependent.matroid_isFlat_iff, natCast_mem, algebraMap_mem, linearEquivOp_symm_apply_coe, mem_star_iff, Localization.localRingHom_bijective_of_saturated_inf_eq_top, mem_adjoin_of_dvd_coeff_of_dvd_aeval, Algebra.TensorProduct.algEquivIncludeRange_symm_toAlgHom, IsPrimitiveRoot.self_sub_one_pow_dvd_order, coe_add, Submodule.lTensorOne_tmul, Algebra.coe_inf, comm_trans_lTensorBot, AlgHom.coe_equalizer, IsPrimitiveRoot.coe_toInteger, CliffordAlgebra.evenEquivEvenNeg_symm_apply, minpoly.instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure, integralClosure.isDedekindDomain_fractionRing, ContinuousMap.polynomial_comp_attachBound, IsPrimitiveRoot.adjoin_isCyclotomicExtension, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, IntermediateField.coe_type_toSubalgebra, CliffordAlgebra.ofEven_ฮน, isAlgebraic_bot_iff, AlgebraicIndependent.iff_adjoin_image, instSMulCommClassSubtypeMemSubalgebraIntegralClosure, toSubring_subtype, IntermediateField.algebraicIndependent_adjoin_iff, instIsDomainSubtypeMemSubalgebraIntegralClosure, integralClosure.isIntegral, IntermediateField.rank_eq_rank_subalgebra, MvPolynomial.mem_symmetricSubalgebra, instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMap, val_comp_inclusion, Set.integer_valuation_le_one, continuousSMul, setRange_algebraMap, centralizer_coe_image_includeLeft_eq_center_tensorProduct, IsScalarTower.subalgebra', Algebra.cardinalMk_adjoin_le, algebraMap_apply, smul_def, integralClosure.isIntegralClosure, MvPolynomial.esymmAlgHom_fin_bijective, IsCyclotomicExtension.adjoin_roots, instFiniteTypeSubtypePolynomialMemSubalgebraReesAlgebraOfIsNoetherianRing, MvPolynomial.esymmAlgEquiv_apply, IsFractionRing.liftAlgHom_fieldRange, val_mulMap'_tmul, mem_pi, IntermediateField.algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin, LinearDisjoint.norm_algebraMap, IntermediateField.equivOfEq_apply, ContinuousMap.polynomial_comp_attachBound_mem, isAlgebraic_iff, IntermediateField.isAlgebraic_adjoin_iff_bot, Algebra.adjoin_union_eq_adjoin_adjoin, Localization.localRingHom_bijective_of_not_conductor_le, IsTranscendenceBasis.isAlgebraic, StarSubalgebra.coe_toSubalgebra, AlgHom.isNoetherianRing_range, Polynomial.aeval_mem_adjoin_singleton, IntermediateField.transcendental_adjoin_iff, mem_prod, IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1, mem_perfectClosure_iff, Algebra.adjoin.powerBasis'_gen, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, range_le, AlgHom.mem_equalizer, isDomain, LinearDisjoint.isDomain, ContinuousAlgHom.instCompleteSpaceSubtypeMemSubalgebraEqualizerOfT2SpaceOfContinuousMapClass, mem_toSubring, isNoetherianRing_of_fg, IsAlgClosed.isAlgClosure_of_transcendence_basis, Submodule.lTensorOne_one_tmul, Submodule.mem_toSubalgebra, IsCyclotomicExtension.union_right, toSubsemiring_subtype, IntermediateField.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap, IsIntegral.inv_mem_adjoin, equivOfEq_symm, Algebra.essFiniteType_iff, coe_centralizer, Algebra.EssFiniteType.cond, ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints, isIntegral_iff, LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton, mulMap_tmul, AlgEquiv.subalgebraMap_symm_apply_coe, coe_toSubring, Algebra.mem_inf, one_mem, coe_pow, finrank_bot, MvPolynomial.supportedEquivMvPolynomial_symm_C, Algebra.coe_sInf, Algebra.sup_def, LinearDisjoint.adjoin_rank_eq_rank_right, LinearDisjoint.basisOfBasisLeft_repr_apply, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, CliffordAlgebra.evenToNeg_comp_evenToNeg, MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_le, Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver, mopAlgEquivOp_apply_coe, instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure, MvPolynomial.transcendental_supported_X, coe_mk, IsLocalization.Away.integralClosure, isClosed_topologicalClosure, LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, algEquivOpMop_symm_apply_coe, CyclotomicRing.eq_adjoin_primitive_root, rTensorBot_tmul, LinearDisjoint.rank_eq_one_of_flat_of_self_of_inj, range_algebraMap, AlgebraicIndependent.iff_transcendental_adjoin_image, Module.End.exists_isNilpotent_isSemisimple, isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic, instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra, integralClosure.mem_lifts_of_monic_of_dvd_map, IsCyclotomicExtension.lcm_sup, topologicalClosure_adjoin_le_centralizer_centralizer, rank_bot, coe_valA', MvPolynomial.supported_eq_vars_subset, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, notMem_iff_exists_ne_and_isConjRoot, Algebra.gc, rank_toSubmodule, Transcendental.integralClosure, Algebra.botEquiv_symm_apply, RingCon.coe_quotientKerEquivRangeโ_mkโ, Ideal.Filtration.submodule_fg_iff_stable, Module.End.mem_subalgebraCenter_iff, rank_top, Algebra.TensorProduct.linearEquivIncludeRange_tmul, Algebra.Smooth.exists_subalgebra_fg, finrank_eq_one_iff, MvPolynomial.esymmAlgHom_surjective, CommRingCat.Under.equalizer_comp, centralizer_range_includeRight_eq_center_tensorProduct, subalgebra_top_rank_eq_submodule_top_rank, MvPolynomial.esymmAlgEquiv_symm_apply, equivOfEq_trans, Localization.mem_range_mapToFractionRing_iff, CommRingCat.Under.equalizerFork'_ฮน, coe_inclusion, Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg, FunctionField.ringOfIntegers.not_isField, CliffordAlgebra.even.lift.aux_one, finite_bot, MvPolynomial.esymmAlgHom_injective, Algebra.self_mem_adjoin_singleton, ext_iff, coe_prod, Algebra.rank_adjoin_le, MvPolynomial.renameSymmetricSubalgebra_apply_coe, CliffordAlgebra.even.lift.aux_algebraMap, MvPolynomial.transcendental_supported_polynomial_aeval_X, Localization.subalgebra.instIsFractionRingSubtypeMemSubalgebra, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective, mem_centralizer_iff
|
map ๐ | CompOp | 51 mathmath: map_mono, Algebra.TensorProduct.includeLeft_map_center_le, topologicalClosure_map, comap_map_eq, centralizer_coe_map_includeLeft_eq_center_tensorProduct, integralClosure_map_algEquiv, Algebra.map_sup, mulMap_map_comp_eq, comap_map_eq_self_of_injective, map_comap_eq_self, Algebra.map_bot, mem_adjoin_map_integralClosure_of_isStandardEtale, IntermediateField.toSubalgebra_map, Algebra.TensorProduct.includeRight_map_center_le, Algebra.map_inf, gc_map_comap, centralizer_coe_map_includeRight_eq_center_tensorProduct, FG.map, coe_equivMapOfInjective_apply, mem_map, topologicalClosure_map_le, LinearDisjoint.map, DenseRange.topologicalClosure_map_subalgebra, AlgHom.map_adjoin, StarSubalgebra.map_toSubalgebra, map_le, map_toSubmodule, map_injective, map_id, Algebra.adjoin_image, coe_map, AlgEquiv.subalgebraMap_apply_coe, map_comap_eq_self_of_surjective, AlgHom.subalgebraMap_coe_apply, Algebra.EssFiniteType.aux, map_topologicalClosure_le, Algebra.adjoin_restrictScalars, AlgHom.subalgebraMap_surjective, range_comp_val, Matrix.subalgebraCenter_eq_scalarAlgHom_map, map_comap_eq, Algebra.map_top, Algebra.adjoin_algebraMap, AlgHom.map_adjoin_singleton, Algebra.map_iInf, comap_map_eq_self, AlgEquiv.subalgebraMap_symm_apply_coe, map_toSubsemiring, AlgHom.range_comp, map_map, RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict
|
module' ๐ | CompOp | 1 mathmath: instIsScalarTowerSubtypeMem
|
moduleLeft ๐ | CompOp | 22 mathmath: Ideal.Filtration.submodule_closure_single, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, Ideal.Filtration.mem_submodule, instIsTorsionFree', LinearDisjoint.linearIndependent_left_op_of_flat, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, LinearDisjoint.algebraMap_basisOfBasisRight_apply, Ideal.Filtration.inf_submodule, LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, Ideal.Filtration.submodule_span_single, exists_subalgebra_of_fg, Algebra.Smooth.exists_subalgebra_finiteType, LinearDisjoint.linearIndependent_right_of_flat, Algebra.Etale.exists_subalgebra_fg, LinearDisjoint.basisOfBasisLeft_apply, LinearDisjoint.linearIndependent_left_of_flat_of_commute, LinearDisjoint.linearIndependent_left_of_flat, LinearDisjoint.basisOfBasisLeft_repr_apply, LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, Ideal.Filtration.submodule_fg_iff_stable, Algebra.Smooth.exists_subalgebra_fg, Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg
|
ofClass ๐ | CompOp | 1 mathmath: coe_ofClass
|
toAddSubmonoid ๐ | CompOp | 1 mathmath: coe_toAddSubmonoid
|
toAlgebra ๐ | CompOp | 102 mathmath: AlgebraicIndependent.transcendental_adjoin_iff, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow, Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin, AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic, Localization.isFractionRing_range_mapToFractionRing, finrank_sup_eq_finrank_right_mul_finrank_of_free, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, AlgebraicIndependent.transcendental_adjoin, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, rank_sup_eq_rank_left_mul_rank_of_free, AlgebraicIndependent.iff_adjoin_image_compl, LinearDisjoint.adjoin_rank_eq_rank_left, FunctionField.ringOfIntegers.instIsIntegralClosureSubtypeMemSubalgebraPolynomial, AlgebraicIndependent.matroid_isBasis_iff, algebra_isAlgebraic_bot_left_iff, IsScalarTower.adjoin_range_toAlgHom, IntermediateField.isAlgebraic_adjoin_iff_top, IsIntegrallyClosedIn.exists_algebraMap_eq_of_pow_mem_subalgebra, integralClosure_idem, AlgebraicIndependent.adjoin_iff_disjoint, IntermediateField.isAlgebraic_adjoin_iff, AlgebraicIndependent.matroid_spanning_iff, range_isScalarTower_toAlgHom, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, algebraMap_mk, prod_mem_ideal_map_of_mem_conductor, LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply, MvPolynomial.transcendental_supported_X_iff, algebraMap_def, AlgebraicIndependent.sumElim_iff, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, integralClosure.isFractionRing_of_finite_extension, AlgebraicIndependent.adjoin_of_disjoint, Algebra.essFiniteType_cond_iff, IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebra, AlgebraicIndependent.subalgebraAlgebraicClosure, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, LinearDisjoint.algebraMap_basisOfBasisRight_apply, LinearDisjoint.trace_algebraMap, AlgebraicIndependent.isAlgebraic_adjoin_iff_of_matroid_isBasis, Algebra.Presentation.instHasCoeffsSubtypeMemSubalgebraAdjoin, Algebra.EssFiniteType.isLocalization, AlgebraicIndependent.option_iff_transcendental, AlgebraicIndependent.algebraMap_aevalEquiv, MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero, algebraMap_eq, instIsIntegrallyClosedInSubtypeMemSubalgebraIntegralClosure, finrank_sup_eq_finrank_left_mul_finrank_of_free, IntermediateField.isTranscendenceBasis_adjoin_iff, integralClosure.isFractionRing_of_algebraic, AlgebraicIndepOn.insert_iff, Algebra.Smooth.exists_subalgebra_finiteType, rank_sup_eq_rank_right_mul_rank_of_free, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, Algebra.Etale.exists_subalgebra_fg, isAlgebraic_iff_exists_isTranscendenceBasis_subset, Algebra.adjoin_top, Localization.subalgebra.isFractionRing, Algebra.essFiniteType_iff_exists_subalgebra, Algebra.restrictScalars_adjoin, Transcendental.subalgebraAlgebraicClosure, rangeS_algebraMap, Localization.subalgebra.isFractionRing_ofField, FunctionField.ringOfIntegers.instIsFractionRingSubtypeMemSubalgebraPolynomial, Algebra.adjoin_restrictScalars, LinearDisjoint.basisOfBasisLeft_apply, LinearDisjoint.mulMapLeftOfSupEqTop_tmul, AlgebraicIndependent.option_iff, AlgebraicIndependent.matroid_closure_eq, AlgebraicIndependent.integralClosure, Localization.localRingHom_bijective_of_saturated_inf_eq_top, isAlgebraic_bot_iff, AlgebraicIndependent.iff_adjoin_image, IntermediateField.algebraicIndependent_adjoin_iff, setRange_algebraMap, algebraMap_apply, integralClosure.isIntegralClosure, LinearDisjoint.norm_algebraMap, Algebra.adjoin_union_eq_adjoin_adjoin, Localization.localRingHom_bijective_of_not_conductor_le, IsTranscendenceBasis.isAlgebraic, IntermediateField.transcendental_adjoin_iff, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, IsAlgClosed.isAlgClosure_of_transcendence_basis, IsCyclotomicExtension.union_right, Algebra.EssFiniteType.cond, LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton, LinearDisjoint.adjoin_rank_eq_rank_right, LinearDisjoint.basisOfBasisLeft_repr_apply, MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_le, MvPolynomial.transcendental_supported_X, range_algebraMap, AlgebraicIndependent.iff_transcendental_adjoin_image, isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic, integralClosure.mem_lifts_of_monic_of_dvd_map, Transcendental.integralClosure, Algebra.Smooth.exists_subalgebra_fg, Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg, MvPolynomial.transcendental_supported_polynomial_aeval_X, Localization.subalgebra.instIsFractionRingSubtypeMemSubalgebra
|
toCommRing ๐ | CompOp | 97 mathmath: AlgebraicIndependent.transcendental_adjoin_iff, algebraicIndependent_adjoin, AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic, finrank_sup_eq_finrank_right_mul_finrank_of_free, TensorProduct.toIntegralClosure_bijective_of_isLocalization, AlgebraicIndependent.transcendental_adjoin, integralClosure.isIntegrallyClosedOfFiniteExtension, rank_sup_eq_rank_left_mul_rank_of_free, AlgebraicIndependent.iff_adjoin_image_compl, LinearDisjoint.adjoin_rank_eq_rank_left, IntermediateField.algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin, AlgebraicIndependent.matroid_isBasis_iff, algebra_isAlgebraic_bot_left_iff, TensorProduct.toIntegralClosure_bijective_of_smooth, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, IntermediateField.isAlgebraic_adjoin_iff_top, integralClosure_idem, AlgebraicIndependent.adjoin_iff_disjoint, IntermediateField.isAlgebraic_adjoin_iff, AlgebraicIndependent.matroid_spanning_iff, integralClosure.isDedekindDomain, AlgebraicGeometry.Scheme.Hom.ฮน_toNormalization, MvPolynomial.transcendental_supported_X_iff, LinearDisjoint.rank_sup_of_free, NumberField.RingOfIntegers.mk_mul_mk, AlgebraicIndependent.sumElim_iff, Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, AlgHom.coe_tensorEqualizer, TensorProduct.toIntegralClosure_mvPolynomial_bijective, AlgebraicIndependent.adjoin_of_disjoint, finrank_right_dvd_finrank_sup_of_free, AlgebraicIndependent.subalgebraAlgebraicClosure, isNoetherian_adjoin_finset, CommRingCat.Under.tensorProdEqualizer_ฮน, isCyclotomicExtension_iff_eq_adjoin, NumberField.RingOfIntegers.mk_add_mk, FunctionField.ringOfIntegers.instIsIntegrallyClosedSubtypeMemSubalgebraPolynomial, LinearDisjoint.trace_algebraMap, AlgebraicIndependent.isAlgebraic_adjoin_iff_of_matroid_isBasis, finrank_left_dvd_finrank_sup_of_free, IntermediateField.finrank_eq_finrank_subalgebra, Algebra.Presentation.instHasCoeffsSubtypeMemSubalgebraAdjoin, AlgebraicIndependent.option_iff_transcendental, instIsIntegrallyClosedInSubtypeMemSubalgebraIntegralClosure, AlgHom.tensorEqualizerEquiv_apply, Algebra.finite_adjoin_of_finite_of_isIntegral, finrank_sup_eq_finrank_left_mul_finrank_of_free, finrank_sup_le_of_free, IntermediateField.isTranscendenceBasis_adjoin_iff, Ring.DimensionLEOne.integralClosure, AlgebraicIndepOn.insert_iff, Algebra.Smooth.exists_subalgebra_finiteType, rank_sup_eq_rank_right_mul_rank_of_free, Algebra.Etale.exists_subalgebra_fg, isAlgebraic_iff_exists_isTranscendenceBasis_subset, FunctionField.ringOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc, isCyclotomicExtension_singleton_iff_eq_adjoin, LinearDisjoint.rank_inf_eq_one_of_flat_left_of_inj, AlgebraicGeometry.Scheme.Hom.ฮน_toNormalization_assoc, LinearDisjoint.finrank_sup_of_free, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, IsCyclotomicExtension.union_left, Transcendental.subalgebraAlgebraicClosure, rank_sup_le_of_free, TensorProduct.toIntegralClosure_injective_of_flat, LinearDisjoint.rank_inf_eq_one_of_flat_right_of_inj, AlgebraicIndependent.option_iff, AlgebraicIndependent.matroid_closure_eq, AlgebraicIndependent.integralClosure, FunctionField.ringOfIntegers.instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc, CommRingCat.Under.equalizerFork_ฮน, integralClosure.isDedekindDomain_fractionRing, isAlgebraic_bot_iff, AlgebraicIndependent.iff_adjoin_image, IntermediateField.algebraicIndependent_adjoin_iff, IntermediateField.rank_eq_rank_subalgebra, LinearDisjoint.norm_algebraMap, IsTranscendenceBasis.isAlgebraic, IntermediateField.transcendental_adjoin_iff, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, IsAlgClosed.isAlgClosure_of_transcendence_basis, IsCyclotomicExtension.union_right, LinearDisjoint.adjoin_rank_eq_rank_right, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_le, MvPolynomial.transcendental_supported_X, LinearDisjoint.rank_eq_one_of_flat_of_self_of_inj, AlgebraicIndependent.iff_transcendental_adjoin_image, isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic, IsCyclotomicExtension.lcm_sup, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, Transcendental.integralClosure, Algebra.Smooth.exists_subalgebra_fg, CommRingCat.Under.equalizer_comp, CommRingCat.Under.equalizerFork'_ฮน, Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg, MvPolynomial.transcendental_supported_polynomial_aeval_X
|
toCommSemiring ๐ | CompOp | 66 mathmath: Localization.subalgebra.isLocalization_subalgebra, Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin, Localization.isFractionRing_range_mapToFractionRing, finrank_sup_eq_finrank_right_mul_finrank_of_free, Localization.isLocalization_range_mapToFractionRing, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, rank_sup_eq_rank_left_mul_rank_of_free, LinearDisjoint.adjoin_rank_eq_rank_left, FunctionField.ringOfIntegers.instIsIntegralClosureSubtypeMemSubalgebraPolynomial, IsScalarTower.adjoin_range_toAlgHom, IsIntegrallyClosedIn.exists_algebraMap_eq_of_pow_mem_subalgebra, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, range_isScalarTower_toAlgHom, algebraMap_mk, LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply, algebraMap_def, integralClosure.isFractionRing_of_finite_extension, Algebra.essFiniteType_cond_iff, IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebra, mvPolynomial_aeval_coe, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, LinearDisjoint.algebraMap_basisOfBasisRight_apply, LinearDisjoint.trace_algebraMap, Localization.subalgebra.isLocalization_ofField, Algebra.EssFiniteType.isLocalization, AlgebraicIndependent.algebraMap_aevalEquiv, MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero, algebraMap_eq, finrank_sup_eq_finrank_left_mul_finrank_of_free, integralClosure.isFractionRing_of_algebraic, Algebra.Smooth.exists_subalgebra_finiteType, rank_sup_eq_rank_right_mul_rank_of_free, Algebra.Etale.exists_subalgebra_fg, Algebra.adjoin_top, Localization.subalgebra.isFractionRing, Algebra.essFiniteType_iff_exists_subalgebra, IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin, Algebra.restrictScalars_adjoin, rangeS_algebraMap, Localization.subalgebra.isFractionRing_ofField, FunctionField.ringOfIntegers.instIsFractionRingSubtypeMemSubalgebraPolynomial, Algebra.adjoin_restrictScalars, LinearDisjoint.basisOfBasisLeft_apply, LinearDisjoint.mulMapLeftOfSupEqTop_tmul, IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin, IsLocalization.integralClosure, Localization.localRingHom_bijective_of_saturated_inf_eq_top, setRange_algebraMap, algebraMap_apply, integralClosure.isIntegralClosure, IntermediateField.algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin, LinearDisjoint.norm_algebraMap, Algebra.adjoin_union_eq_adjoin_adjoin, Localization.localRingHom_bijective_of_not_conductor_le, IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1, Algebra.EssFiniteType.cond, LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, LinearDisjoint.adjoin_rank_eq_rank_right, LinearDisjoint.basisOfBasisLeft_repr_apply, IsLocalization.Away.integralClosure, range_algebraMap, integralClosure.mem_lifts_of_monic_of_dvd_map, Algebra.Smooth.exists_subalgebra_fg, Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg, Localization.subalgebra.instIsFractionRingSubtypeMemSubalgebra, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
|
toNonUnitalSubalgebra ๐ | CompOp | 5 mathmath: NonUnitalAlgebra.adjoin_le_algebra_adjoin, NonUnitalSubalgebra.toSubalgebra_toNonUnitalSubalgebra, Unitization.lift_range_le, one_mem_toNonUnitalSubalgebra, toNonUnitalSubalgebra_toSubalgebra
|
toRing ๐ | CompOp | 49 mathmath: CliffordAlgebra.even.lift.aux_mul, integralClosure.AlgebraIsIntegral, Algebra.IsIntegral.adjoin, algebra_isAlgebraic_bot_right, instSMulDistribClassSubtypeMemSubalgebraIntegralClosure, isSeparable_iff, Algebra.adjoin.powerBasis_dim, FiniteDimensional.of_subalgebra_toSubmodule, CliffordAlgebra.even.lift_ฮน, Algebra.adjoin.powerBasis'_dim, CliffordAlgebra.even.algHom_ext_iff, le_integralClosure_iff_isIntegral, quotAdjoinEquivQuotMap_apply_mk, Algebra.adjoin.powerBasis_gen, LinearDisjoint.rank_eq_one_of_commute_of_flat_of_self_of_inj, ValuationSubring.isIntegral_of_mem_ringOfIntegers', CliffordAlgebra.evenToNeg_ฮน, finiteDimensional_toSubmodule, ValuationSubring.isIntegral_of_mem_ringOfIntegers, minpoly.ofSubring, FiniteDimensional.finiteDimensional_subalgebra, CliffordAlgebra.even.lift_symm_apply_bilin, integralClosure.coe_smul, Algebra.isIntegral_iSup, isAlgebraic_iff_isAlgebraic_val, Algebra.isIntegral_sup, Algebra.adjoin.powerBasis'_minpoly_gen, CliffordAlgebra.even.lift.aux_apply, CliffordAlgebra.even.lift.aux_ฮน, rank_eq_one_iff, LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_left_of_inj, CliffordAlgebra.ofEven_ฮน, instSMulCommClassSubtypeMemSubalgebraIntegralClosure, integralClosure.isIntegral, LinearDisjoint.norm_algebraMap, isAlgebraic_iff, IntermediateField.isAlgebraic_adjoin_iff_bot, Algebra.adjoin.powerBasis'_gen, isIntegral_iff, finrank_bot, LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_right_of_inj, instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure, range_algebraMap, instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra, rank_bot, finrank_eq_one_iff, CliffordAlgebra.even.lift.aux_one, Algebra.rank_adjoin_le, CliffordAlgebra.even.lift.aux_algebraMap
|
toSemiring ๐ | CompOp | 277 mathmath: mulMap_comm, inclusion_right, Submodule.rTensorOne_symm_apply, minpoly.ToAdjoin.injective, Algebra.RingHom.adjoin_algebraMap_apply, Ideal.Filtration.submodule_closure_single, centralizer_tensorProduct_eq_center_tensorProduct_right, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, StarAlgEquiv.ofInjective_symm_apply, adjoin_rank_le, AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm, Algebra.FiniteType.adjoin_of_finite, ValuationSubring.integralClosure_algebraMap_injective, Submodule.comm_trans_lTensorOne, AlgHom.val_comp_codRestrict, LinearDisjoint.sup_free_of_free, Submodule.mulMap_one_right_eq, finrank_sup_eq_finrank_right_mul_finrank_of_free, TensorProduct.toIntegralClosure_bijective_of_isLocalization, equivOfEq_apply, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, AlgHom.rangeRestrict_surjective, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, AlgHom.coe_mapIntegralClosure, AlgebraicIndependent.repr_ker, Set.unitEquivUnitsInteger_symm_apply_coe, AlgEquiv.ofInjective_apply, centralizer_coe_map_includeLeft_eq_center_tensorProduct, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, rank_sup_eq_rank_left_mul_rank_of_free, MvPolynomial.supportedEquivMvPolynomial_symm_X, aeval_coe, LinearDisjoint.adjoin_rank_eq_rank_left, Polynomial.lift_of_splits, mulMap_toLinearMap, Ideal.Filtration.mem_submodule, instIsTorsionFree', RingCon.quotientKerEquivRangeโ_comp_mkโ, RingCon.coe_comapQuotientEquivRangeโ_mk, val_apply, inclusion.isScalarTower_left, comm_trans_rTensorBot, mulMap_map_comp_eq, Algebra.EssFiniteType.adjoin_mem_finset, TensorProduct.toIntegralClosure_bijective_of_smooth, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, Algebra.TensorProduct.algEquivIncludeRange_symm_tmul, AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, AdjoinRoot.Minpoly.toAdjoin.surjective, AlgHom.val_comp_rangeRestrict, LinearDisjoint.linearIndependent_left_op_of_flat, AlgebraicIndependent.aeval_comp_repr, Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, range_isScalarTower_toAlgHom, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, instSMulDistribClassSubtypeMemSubalgebraIntegralClosure, Field.Emb.Cardinal.succEquiv_coherence, AlgebraicGeometry.Scheme.Hom.ฮน_toNormalization, prod_mem_ideal_map_of_mem_conductor, Polynomial.aeval_subalgebra_coe, mopAlgEquivOp_symm_apply, inclusion_inclusion, LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply, TensorProduct.Algebra.exists_of_fg, FunctionField.classNumber_eq_one_iff, coe_mul, centralizer_coe_image_includeRight_eq_center_tensorProduct, instIsTorsionFree, finrank_toSubmodule, lTensorBot_one_tmul, Matrix.isRepresentation.toEnd_represents, mulMap_bot_left_eq, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, CliffordAlgebra.coe_toEven_reverse_involute, AlgHom.coe_tensorEqualizer, TensorProduct.toIntegralClosure_mvPolynomial_bijective, valA_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', Algebra.essFiniteType_cond_iff, ContinuousAlgHom.coe_codRestrict, Algebra.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap, AlgHom.ker_rangeRestrict, AdjoinRoot.Minpoly.coe_toAdjoin, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, FunctionField.ringOfIntegers.instIsDomainSubtypeMemSubalgebraPolynomial, linearEquivOp_apply_coe, topEquiv_apply, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, centralizer_coe_map_includeRight_eq_center_tensorProduct, range_val, AlgEquiv.ofLeftInverse_apply, MvPolynomial.rename_esymmAlgHom, CliffordAlgebra.even.lift_ฮน, mulMap'_surjective, Submodule.comm_trans_rTensorOne, coe_equivMapOfInjective_apply, adjoin_eq_span_basis, isField_of_algebraic, LinearDisjoint.algebraMap_basisOfBasisRight_apply, LinearDisjoint.trace_algebraMap, Matrix.isRepresentation.toEnd_exists_mem_ideal, instIsNoetherianRingSubtypePolynomialMemSubalgebraReesAlgebra, coe_algebraMap, Submodule.lTensorOne'_tmul, Submodule.rTensorOne'_tmul_one, AlgEquiv.coe_mapIntegralClosure, CliffordAlgebra.toEven_comp_ofEven, Ideal.Filtration.inf_submodule, Submodule.rTensorOne'_tmul, ContinuousAlgHom.coe_codRestrict_apply, MvPolynomial.esymmAlgHom_fin_surjective, integralClosure.isNoetherianRing, NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, Set.val_unitEquivUnitsInteger_apply_coe, quotAdjoinEquivQuotMap_apply_mk, LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, equivOfEq_rfl, Ideal.Filtration.submodule_span_single, fg_iff_finiteType, Submodule.rTensorOne_tmul, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient, toIsStrictOrderedRing, inclusion_mk, noZeroDivisors, inclusion_injective, centralizer_tensorProduct_eq_center_tensorProduct_left, Ideal.IntegralClosure.isMaximal_of_isMaximal_comap, AlgebraicIndependent.algebraMap_aevalEquiv, AdjoinRoot.Minpoly.coe_toAdjoin_mk_X, rTensorBot_tmul_one, algebraMap_eq, exists_subalgebra_of_fg, AlgHom.tensorEqualizerEquiv_apply, finrank_sup_eq_finrank_left_mul_finrank_of_free, CliffordAlgebra.evenToNeg_ฮน, Submodule.rTensorOne_tmul_one, inclusion.isScalarTower_right, RingCon.coe_comapQuotientEquivRangeโ_symm_mk, finite_sup, coe_val, mulMap_bot_right_eq, Algebra.TensorProduct.linearEquivIncludeRange_symm_tmul, Algebra.TensorProduct.algEquivIncludeRange_tmul, Algebra.Smooth.exists_subalgebra_finiteType, rank_sup_eq_rank_right_mul_rank_of_free, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, LinearDisjoint.linearIndependent_right_of_flat, lTensorBot_symm_apply, coe_valA, inclusion_self, inclusion.faithfulSMul, RingCon.comapQuotientEquivRangeโ_mk, Submodule.range_valA, Submodule.mulMap_one_left_eq, AlgebraicIndependent.aeval_repr, algEquivOpMop_apply, instIsTopologicalSemiringSubtypeMemSubalgebra, Algebra.adjoin_adjoin_coe_preimage, CliffordAlgebra.ofEven_comp_toEven, MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe, AlgEquiv.subalgebraMap_apply_coe, AlgebraicGeometry.Scheme.Hom.ฮน_toNormalization_assoc, Algebra.TensorProduct.algEquivIncludeRange_toAlgHom, Polynomial.coe_aeval_mk_apply, FunctionField.ringOfIntegers.algebraMap_injective, AlgHom.subalgebraMap_coe_apply, Algebra.essFiniteType_iff_exists_subalgebra, Submodule.exists_fg_of_baseChange_eq_zero, MvPolynomial.esymmAlgHom_fin_injective, CliffordAlgebra.even.lift_symm_apply_bilin, CliffordAlgebra.evenEquivEvenNeg_apply, linearDisjoint_iff_injective, fg_top, CliffordAlgebra.toEven_ฮน, integralClosure.coe_smul, lTensorBot_tmul, topEquiv_symm_apply_coe, TensorProduct.toIntegralClosure_injective_of_flat, Matrix.isRepresentation.toEnd_surjective, AlgEquiv.ofLeftInverse_symm_apply, LinearDisjoint.val_mulMap_tmul, minpoly.equivAdjoin_toAlgHom, RingCon.quotientKerEquivRangeโ_mkโ, MvPolynomial.esymmAlgHom_apply, mulMap_range, LinearDisjoint.basisOfBasisLeft_apply, MvPolynomial.irreducible_toPolynomialAdjoinImageCompl, centralizer_coe_range_includeLeft_eq_center_tensorProduct, AlgebraicIndependent.aevalEquiv_apply_coe, rTensorBot_symm_apply, AlgHom.subalgebraMap_surjective, LinearDisjoint.mulMapLeftOfSupEqTop_tmul, Algebra.RingHom.adjoin_algebraMap_surjective, Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap, range_comp_val, Submodule.lTensorOne_symm_apply, Matrix.isRepresentation.eq_toEnd_of_represents, Algebra.mem_ideal_map_adjoin, instIsScalarTowerSubtypeMem, LinearDisjoint.linearIndependent_left_of_flat_of_commute, Submodule.lTensorOne'_one_tmul, minpoly.coe_equivAdjoin, Algebra.instFiniteTypeSubtypeMemSubalgebraSubalgebra, ContinuousAlgHom.coe_rangeRestrict, toIsOrderedRing, subalgebra_top_finrank_eq_submodule_top_finrank, IsLocalization.integralClosure, linearEquivOp_symm_apply_coe, Algebra.TensorProduct.algEquivIncludeRange_symm_toAlgHom, coe_add, Submodule.lTensorOne_tmul, comm_trans_lTensorBot, CliffordAlgebra.evenEquivEvenNeg_symm_apply, ContinuousMap.polynomial_comp_attachBound, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, CliffordAlgebra.ofEven_ฮน, instSMulCommClassSubtypeMemSubalgebraIntegralClosure, toSubring_subtype, instIsDomainSubtypeMemSubalgebraIntegralClosure, val_comp_inclusion, LinearDisjoint.linearIndependent_left_of_flat, centralizer_coe_image_includeLeft_eq_center_tensorProduct, IsScalarTower.subalgebra', MvPolynomial.esymmAlgHom_fin_bijective, AlgHom.coe_codRestrict, instFiniteTypeSubtypePolynomialMemSubalgebraReesAlgebraOfIsNoetherianRing, MvPolynomial.esymmAlgEquiv_apply, val_mulMap'_tmul, LinearDisjoint.norm_algebraMap, AlgHom.isNoetherianRing_range, isDomain, LinearDisjoint.isDomain, isNoetherianRing_of_fg, Submodule.lTensorOne_one_tmul, AlgHom.injective_codRestrict, toSubsemiring_subtype, equivOfEq_symm, Algebra.EssFiniteType.cond, LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, mulMap_tmul, AlgEquiv.subalgebraMap_symm_apply_coe, MvPolynomial.supportedEquivMvPolynomial_symm_C, LinearDisjoint.adjoin_rank_eq_rank_right, LinearDisjoint.basisOfBasisLeft_repr_apply, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, CliffordAlgebra.evenToNeg_comp_evenToNeg, Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver, mopAlgEquivOp_apply_coe, IsLocalization.Away.integralClosure, LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, algEquivOpMop_symm_apply_coe, rTensorBot_tmul, instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra, mk_algebraMap, coe_valA', rank_toSubmodule, Algebra.botEquiv_symm_apply, RingCon.coe_quotientKerEquivRangeโ_mkโ, Ideal.Filtration.submodule_fg_iff_stable, rank_top, Algebra.TensorProduct.linearEquivIncludeRange_tmul, MvPolynomial.esymmAlgHom_surjective, centralizer_range_includeRight_eq_center_tensorProduct, subalgebra_top_rank_eq_submodule_top_rank, MvPolynomial.esymmAlgEquiv_symm_apply, equivOfEq_trans, coe_inclusion, FunctionField.ringOfIntegers.not_isField, finite_bot, MvPolynomial.esymmAlgHom_injective, comap_map_eq_map_adjoin_of_coprime_conductor, MvPolynomial.renameSymmetricSubalgebra_apply_coe, CliffordAlgebra.even.lift.aux_algebraMap, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
|
toSubmodule ๐ | CompOp | 61 mathmath: integralClosure_le_span_dualBasis, toSubmodule_injective, Submodule.mulMap_one_right_eq, UnitAddTorus.mFourierSubalgebra_coe, mulMap_toLinearMap, Submonoid.adjoin_eq_span_of_eq_span, Algebra.span_le_adjoin, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, mem_toSubmodule, range_isScalarTower_toAlgHom, Algebra.toSubmodule_bot, Algebra.sInf_toSubmodule, finrank_toSubmodule, isIdempotentElem_toSubmodule, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_coeff_minpolyDiv, Algebra.top_toSubmodule, Submodule.toSubalgebra_toSubmodule, traceForm_dualSubmodule_adjoin, FractionalIdeal.adjoinIntegral_coe, mul_toSubmodule, Algebra.adjoin_nonUnitalSubalgebra_eq_span, FractionalIdeal.isFractional_adjoin_integral, mem_integralClosure_iff_mem_fg, adjoin_eq_span_basis, mul_toSubmodule_le, Module.Flat.instSubalgebraToSubmodule, Algebra.adjoin_toSubmodule_le, LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, Algebra.inf_toSubmodule, Algebra.adjoin_eq_span_of_subset, linearDisjoint_iff, map_toSubmodule, Submodule.span_range_natDegree_eq_adjoin, Algebra.iInf_toSubmodule, fourierSubalgebra_coe, finiteDimensional_toSubmodule, toSubmodule_toSubalgebra, Algebra.adjoin_union_coe_submodule, Submodule.mulMap_one_left_eq, fg_adjoin_of_finite, Algebra.adjoin_eq_span, CliffordAlgebra.even_toSubmodule, Algebra.toSubmodule_eq_top, pi_toSubsemiring, coe_pi, coe_toSubmodule, restrictScalars_toSubmodule, StarAlgebra.adjoin_eq_span, Submodule.iSup_eq_toSubmodule_range, IsIntegral.fg_adjoin_singleton, MvPolynomial.range_mapAlgHom, FiniteDimensional.subalgebra_toSubmodule, pointwise_smul_toSubmodule, prod_toSubmodule, LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, AlgHom.equalizer_toSubmodule, pi_toSubmodule, rank_toSubmodule, fg_bot_toSubmodule, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
|
toSubmoduleEquiv ๐ | CompOp | โ |
toSubring ๐ | CompOp | 20 mathmath: Algebra.toSubring_eq_top, toSubring_injective, instIsIntegrallyClosedInSubtypeMemSubringToSubringIntegralClosure, Algebra.toSubring_bot, toSubring_toSubsemiring, Subring.integralClosure_subring_le_iff, iInf_valuationSubring_superset, Algebra.adjoin_eq_ring_closure, unop_toSubring, Algebra.top_toSubring, op_toSubring, Subring.integralClosure_le_iff, toSubring_inj, toSubring_subtype, center_toSubring, Set.integer_eq, mem_toSubring, coe_toSubring, range_algebraMap, pointwise_smul_toSubring
|
toSubsemiring ๐ | CompOp | 49 mathmath: op_toSubsemiring, coe_toAddSubmonoid, center_toSubsemiring, Submodule.toSubalgebra_toSubsemiring, IntermediateField.mem_carrier, Algebra.toSubsemiring_eq_top, StarSubalgebra.toNonUnitalStarSubalgebra_toStarSubalgebra, toSubring_toSubsemiring, mopAlgEquivOp_symm_apply, Algebra.sInf_toSubsemiring, VonNeumannAlgebra.centralizer_centralizer', Algebra.sup_toSubsemiring, subalgebraOfSubsemiring_toSubsemiring, linearEquivOp_apply_coe, mem_carrier, Algebra.iSup_toSubsemiring, copy_toSubsemiring, AlgHom.equalizer_toSubsemiring, algebraMap_mem', Algebra.sSup_toSubsemiring, subalgebraOfSubring_toSubsemiring, coe_matrix, Algebra.iInf_toSubsemiring, Algebra.top_toSubsemiring, coe_toSubsemiring, StarSubalgebra.rangeS_le, comap_toSubsemiring, StarSubalgebra.mem_carrier, coe_valA, toSubsemiring_injective, algEquivOpMop_apply, AlgEquiv.subalgebraMap_apply_coe, pi_toSubsemiring, toSubsemiring_inj, mem_toSubsemiring, rangeS_algebraMap, unop_toSubsemiring, linearEquivOp_symm_apply_coe, pointwise_smul_toSubsemiring, Algebra.adjoin_toSubsemiring, toSubsemiring_subtype, AlgEquiv.subalgebraMap_symm_apply_coe, map_toSubsemiring, mopAlgEquivOp_apply_coe, algEquivOpMop_symm_apply_coe, rangeS_le, Algebra.inf_toSubsemiring, coe_valA', AlgHom.range_toSubsemiring
|
val ๐ | CompOp | 42 mathmath: centralizer_tensorProduct_eq_center_tensorProduct_right, AlgHom.val_comp_codRestrict, centralizer_coe_map_includeLeft_eq_center_tensorProduct, val_apply, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgHom.val_comp_rangeRestrict, LinearDisjoint.linearIndependent_left_op_of_flat, AlgebraicIndependent.aeval_comp_repr, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, AlgebraicGeometry.Scheme.Hom.ฮน_toNormalization, TensorProduct.Algebra.exists_of_fg, centralizer_coe_image_includeRight_eq_center_tensorProduct, mulMap_bot_left_eq, AlgHom.coe_tensorEqualizer, CommRingCat.Under.tensorProdEqualizer_ฮน, centralizer_coe_map_includeRight_eq_center_tensorProduct, range_val, LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, centralizer_tensorProduct_eq_center_tensorProduct_left, algebraMap_eq, coe_val, mulMap_bot_right_eq, LinearDisjoint.linearIndependent_right_of_flat, AlgebraicGeometry.Scheme.Hom.ฮน_toNormalization_assoc, Submodule.exists_fg_of_baseChange_eq_zero, StarSubalgebra.toSubalgebra_subtype, centralizer_coe_range_includeLeft_eq_center_tensorProduct, range_comp_val, LinearDisjoint.linearIndependent_left_of_flat_of_commute, CommRingCat.Under.equalizerFork_ฮน, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, toSubring_subtype, val_comp_inclusion, LinearDisjoint.linearIndependent_left_of_flat, centralizer_coe_image_includeLeft_eq_center_tensorProduct, toSubsemiring_subtype, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, CommRingCat.Under.equalizer_comp, centralizer_range_includeRight_eq_center_tensorProduct, CommRingCat.Under.equalizerFork'_ฮน, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
|