AlgHom đ | CompData | 2032 mathmath: CommRingCat.tensorProd_map_right, CliffordAlgebra.unop_reverseOp, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, MvPolynomial.joinâ_rename, IsSymmetricAlgebra.lift_eq, Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt, MvPolynomial.aeval_sum, WeierstrassCurve.baseChange_ΚSq, WittVector.bindâ_frobeniusPoly_wittPolynomial, AlgCat.hom_inv_apply, LinearMap.restrictScalars_toMatrix, ContinuousAlgHom.coe_mk', Algebra.normalizedTrace_map, Ideal.Quotient.exists_algHom_fixedPoint_quotient_under, CliffordAlgebra.toBaseChange_reverse, AlgHom.coe_toLinearMap, WeierstrassCurve.Affine.baseChange_nonsingular, RatFunc.laurent_injective, TensorAlgebra.ofDirectSum_of_tprod, AlgHom.mem_range_self, Bialgebra.comulAlgHom_apply, Subalgebra.inclusion_right, PowerSeries.hasSum_aeval, Polynomial.rootSet_mapsTo, minpoly.ToAdjoin.injective, Polynomial.mem_aroots', IsLocalization.Away.mapâ_surjective_of_surjective, CommAlgCat.comp_apply, Field.Emb.Cardinal.equivLim_coherence, SymmetricAlgebra.lift_Îč_apply, Ideal.comap_fiberIsoOfBijectiveResidueField_apply, AddMonoidAlgebra.lift_apply', MvPolynomial.algHom_ext_iff, MvPolynomial.map_bindâ, IntermediateField.exists_algHom_adjoin_of_splits, CliffordAlgebra.involute_eq_of_mem_odd, Algebra.Generators.aeval_val_surjective, IsSeparable.map, PowerSeries.constantCoeff_expand, WeierstrassCurve.Projective.Equation.baseChange, IntermediateField.aeval_gen_minpoly, AlgEquiv.toAlgHom_toRingHom, DoubleQuot.liftSupQuotQuotMkâ_toRingHom, derivationToSquareZeroOfLift_apply, polynomialFunctions.eq_adjoin_X, wittPolynomial_zmod_self, isSeparable_map_iff, Polynomial.roots_expand, ContinuousAlgHom.toAlgHomMonoidHom_apply, Pi.constAlgHom_apply, Polynomial.algEquivCMulXAddC_apply, ExteriorAlgebra.GradedAlgebra.liftÎč_eq, IntermediateField.algHomEquivAlgHomOfSplits_symm_apply, Polynomial.coe_taylorAlgHom, AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm, LinearMap.exists_monic_and_aeval_eq_zero, AddMonoidAlgebra.algHom_ext'_iff, MvPolynomial.exists_finset_rename, PiTensorProduct.liftAlgHom_apply, AlgHom.comp_toRingHom, Polynomial.expand_contract, AnalyticOn.aeval_polynomial, exists_isIntegral_sub_of_isIntegralElem_of_mul_mem_range, PowerBasis.exists_eq_aeval, Polynomial.algebraMap_pi_eq_aeval, RatFunc.coe_mapAlgHom_eq_coe_map, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, StandardEtalePair.inv_aeval_X_g, ContMDiffMap.coeFnAlgHom_apply, Polynomial.expand_eq_sum, WittVector.aeval_verschiebung_poly', PowerSeries.heval_C, polynomial_smul_apply', Polynomial.continuous_aeval, MvPolynomial.rTensorAlgEquiv_apply, CliffordAlgebraComplex.ofComplex_conj, Ideal.comap_comapâ, AlgHom.coe_toRingHom, Matrix.pow_eq_aeval_mod_charpoly, IntermediateField.algHomEquivAlgHomOfSplits_apply_apply, WeierstrassCurve.Jacobian.baseChange_add, Polynomial.derivWithin_aeval, AlgHom.coe_ringHom_injective, eval_minpolyDiv_self, MvPolynomial.evalâ_expand, Differential.algHom_deriv, Polynomial.disjoint_ker_aeval_of_isCoprime, MvPolynomial.universalFactorizationMap_comp_map, MvPolynomial.aeval_algebraMap_eq_zero_iff, Polynomial.aeval_primPart_eq_zero, MvPowerSeries.support_expand, PolynomialModule.smul_def, FiniteField.nonempty_algHom_of_finrank_dvd, IsAdjoinRoot.mem_ker_map, AlgHom.ker_coe, PowerSeries.coeff_expand_mul, IntermediateField.exists_algHom_of_adjoin_splits', Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, evalâ_minpolyDiv_self, MvPolynomial.expand_X, AlgHom.coe_addMonoidHom_injective, Polynomial.aeval_algebraMap_eq_zero_iff, SkewMonoidAlgebra.algHom_ext'_iff, ConjRootClass.aeval_minpoly_iff, PowerSeries.expand_subst, PowerSeries.expand_apply, Polynomial.contract_expand, CliffordAlgebra.involute_prod_map_Îč, SkewMonoidAlgebra.lift_apply', ExteriorAlgebra.lift_symm_apply, WittVector.ghostComponent_apply, DoubleQuot.coe_quotQuotEquivQuotOfLEâ_symm, aeval_wittPolynomial, RatFunc.laurent_X, AlgHom.toRingHom_toRatAlgHom, WeierstrassCurve.Projective.baseChange_negDblY, NumberField.InfinitePlace.IsUnramified.comap_algHom, Polynomial.fiberEquivQuotient_tmul, hensels_lemma, MvPolynomial.rename_rename, Algebra.TensorProduct.congr_symm_apply, CommAlgCat.inv_hom_apply, Algebra.norm_eq_matrix_det, Representation.asAlgebraHom_single, Subalgebra.comap_map_eq, Algebra.Generators.toAlgHom_ofComp_localizationAway, CliffordAlgebraQuaternion.toQuaternion_star, TensorProduct.toIntegralClosure_bijective_of_isLocalization, Polynomial.mem_rootSet_of_injective, PowerBasis.lift_aeval, Algebra.TensorProduct.mapOfCompatibleSMul_surjective, Polynomial.aeval_map_algebraMap, TensorAlgebra.toTrivSqZeroExt_Îč, MonoidAlgebra.algHom_ext'_iff, evalâ_minpolyDiv_of_evalâ_eq_zero, GradedTensorProduct.lift_tmul, MvPowerSeries.trunc'_expand_trunc', WeierstrassCurve.baseChange_preΚ, Algebra.lmul_algebraMap, AlgHom.comp_algebraMap, Unitization.splitMul_apply, TensorAlgebra.Îč_comp_lift, StandardEtalePair.homEquiv_symm_apply, minpoly.eq_iff_aeval_eq_zero, Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, PolyEquivTensor.right_inv, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, MvPolynomial.aeval_X_left_apply, Polynomial.toPowerSeries_toMvPowerSeries, PolynomialModule.aeval_equivPolynomial, PowerSeries.order_expand, MvPolynomial.expand_eq_zero, CliffordAlgebra.lift_Îč_apply, Algebra.FormallyUnramified.lmul_elem, DualNumber.range_lift, DoubleQuot.coe_quotQuotMkâ, Polynomial.coeff_zero_of_isScalarTower, WeierstrassCurve.Jacobian.baseChange_polynomialZ, FreeAlgebra.lift_comp_Îč, AlgHom.rangeRestrict_surjective, Irreducible.natSepDegree_eq_one_iff_of_monic', TensorAlgebra.toDirectSum_tensorPower_tprod, MonoidAlgebra.tensorEquiv.invFun_tmul, Polynomial.rootMultiplicity_expand_pow, Polynomial.aeval_iterate_derivative_of_ge, Polynomial.derivative_expand, Polynomial.aeval_fn_apply, StandardEtalePresentation.toPresentation_algebra_smul, IsSymmetricAlgebra.equiv_apply, sum_smul_minpolyDiv_eq_X_pow, Polynomial.Monic.natSepDegree_eq_one_iff_of_irreducible', AlgHomClass.toRingHom_toAlgHom, AlgHom.coe_mk, AlgHom.coe_mapIntegralClosure, AlgebraicIndependent.polynomial_aeval_of_transcendental, MvPowerSeries.mapAlgHom_apply, Polynomial.aevalAevalEquiv_apply_apply, AlgHom.algHomClass, MvPolynomial.algHom_ext'_iff, IntermediateField.mem_adjoin_iff, RatFunc.laurent_algebraMap, AlgebraicIndependent.repr_ker, AlgHom.IsArithFrobAt.mk_apply, AlgHom.liftEquiv_symm_apply, chevalley_mvPolynomial_mvPolynomial, IntermediateField.exists_algHom_of_adjoin_splits_of_aeval, DoubleQuot.coe_quotLeftToQuotSupâ, MvPolynomial.aeval_X, IntermediateField.algHomEquivAlgHomOfSplits_apply, eval_minpolyDiv_of_aeval_eq_zero, Rep.to_Module_monoidAlgebra_map_aux, Field.finSepDegree_eq_of_isAlgClosed, AlgEquiv.ofInjective_apply, AdicCompletion.val_smul_eq_evalâ_smul, CliffordAlgebra.op_reverse, AlgCat.forget_obj, CliffordAlgebra.range_lift, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, FiniteField.frobeniusAlgHom_apply, WeierstrassCurve.baseChange_preΚâ, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, CliffordAlgebra.reverse_involute_commute, Module.AEval.of_symm_smul, Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, Polynomial.isFixedPt_newtonMap_of_isUnit_iff, MvPolynomial.optionEquivLeft_apply, minpoly_algHom_toLinearMap, polynomialFunctions.le_equalizer, AlgCat.inv_hom_apply, Algebra.smul_leftMulMatrix, MvPolynomial.ACounit_X, MvPolynomial.prime_rename_iff, IsIntegralClosure.algebraMap_lift, bindâ_xInTermsOfW_wittPolynomial, CommAlgCat.forgetâ_commRingCat_obj, MvPowerSeries.substAlgHom_X, Polynomial.cyclotomic_expand_eq_cyclotomic_mul, MvPolynomial.constantCoeff_rename, MvPowerSeries.continuous_aeval, CliffordAlgebra.equivBaseChange_symm_apply, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, Algebra.map_leftMulMatrix_localization, Algebra.normalizedTrace_comp_algHom, PowerSeries.mapAlgHom_apply, IntermediateField.exists_algHom_of_adjoin_splits, isConjRoot_algHom_iff, AlgHom.coe_coe, RatFunc.laurent_div, CliffordAlgebraQuaternion.toQuaternion_ofQuaternion, Polynomial.aevalEquiv_apply, CommRingCat.free_map_coe, Module.Basis.toMatrix_smul, DoubleQuot.quotQuotEquivQuotOfLEâ_symm_toRingEquiv, IsScalarTower.coe_toAlgHom', TensorAlgebra.Îč_def, MvPowerSeries.coe_substAlgHom, Algebra.lmul_injective, WeierstrassCurve.Projective.baseChange_negAddY, Polynomial.aeval_sumIDeriv, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, minpoly.aux_inj_roots_of_min_poly, Bialgebra.counitAlgHom_apply, Subalgebra.aeval_coe, Polynomial.lift_of_splits, CliffordAlgebraComplex.ofComplex_toComplex, MvPolynomial.ACounit_surjective, AddMonoidAlgebra.lift_mapRangeRingHom_algebraMap, MvPowerSeries.rename_map, WeierstrassCurve.Projective.baseChange_negY, isAlgebraic_algHom_iff, UniversalEnvelopingAlgebra.lift_unique, RingQuot.mkAlgHom_surjective, Field.nonempty_algHom_of_exist_roots, DoubleQuot.quotQuotEquivComm_symmâ, Ideal.Quotient.coe_factorâ, Polynomial.aeval_iterate_derivative_self, MvPolynomial.aeval_eq_eval, AddMonoidAlgebra.mapAlgHom_single, PowerSeries.coeff_heval, Module.endTensorEndAlgHom_apply, MvPolynomial.aeval_ite_mem_eq_self, CliffordAlgebra.toProd_Îč_tmul_one, AlgHom.coe_fn_inj, RingCon.quotientKerEquivRangeâ_comp_mkâ, Algebra.TensorProduct.comm_comp_map_apply, MvPolynomial.evalâHom_C_id_eq_joinâ, PowerSeries.aeval_eq_sum, PolyEquivTensor.toFunAlgHom_apply_tmul, PolynomialLaw.exists_lift', Representation.asAlgebraHom_def, CliffordAlgebra.commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_right, RingCon.coe_comapQuotientEquivRangeâ_mk, Finite.algHom, MvPolynomial.eval_rename_prod_mk, AdjoinRoot.algHom_ext_iff, PowerBasis.equivAdjoinSimple_symm_aeval, TrivSqZeroExt.map_inr, IsLocalization.Away.mapâ_injective_of_injective, MvPolynomial.aevalTower_comp_C, Polynomial.toAddCircle_X_pow_eq_fourier, Subalgebra.val_apply, IsAdjoinRoot.liftHom_root, MvPolynomial.rename_msymm, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd, AlgHom.coe_range, RingHom.toRatAlgHom_apply, IsAlgebraic.algHom, finrank_algHom, MvPolynomial.evalâHom_C_eq_bindâ, RatFunc.liftAlgHom_injective, gelfandTransform_bijective, AlgHom.coe_id, Polynomial.differentiableOn_aeval, Polynomial.aeval_pow_two_pow_dvd_aeval_iterate_newtonMap, CliffordAlgebra.Îč_range_map_lift, transcendental_iff_injective, Algebra.TensorProduct.map_tmul, AlgHom.op_apply_apply, AlgEquiv.toAlgHom_op, AlgHom.coe_ringHom_mk, TensorProduct.toIntegralClosure_bijective_of_smooth, MvPolynomial.rename_id_apply, Algebra.toMatrix_lmul_eq, AddMonoidAlgebra.toRingHom_mapAlgHom, IsCyclotomicExtension.aeval_zeta, MvPowerSeries.expand_mul, Ideal.comap_idâ, Ideal.Quotient.factorâ_apply_mk, Algebra.IsAlgebraic.algHom_bijective, Polynomial.bernoulli_generating_function, AlgHom.ext_iff, Unitization.nnnorm_def, MonoidAlgebra.lift_symm_apply, RingHom.toRatAlgHom_toRingHom, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, MvPolynomial.pderiv_rename, AdjoinRoot.algHom_ext'_iff, Algebra.Presentation.comp_relation_inr, AdjoinRoot.liftAlgHom_of, IsFractionRing.algHom_commutes, RatFunc.Luroth.algEquiv_apply, MonoidAlgebra.coe_liftNCAlgHom, CommAlgCat.ofHom_apply, DualNumber.lift_apply_eps, AdjoinRoot.Minpoly.toAdjoin.surjective, GradedAlgHom.coe_algHom_injective, Algebra.TensorProduct.includeRight_apply, Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat, Polynomial.aeval_X_pow, AlgHom.extendScalarsOfSurjective_apply, Polynomial.Bivariate.aveal_eq_map_swap, MvPolynomial.support_killCompl, WeierstrassCurve.baseChange_ΚâSq, Polynomial.integralNormalization_aeval_eq_zero, IsLocalizedModule.map_linearMap_of_isLocalization, AlgEquiv.ofBijective_symm_apply_apply, MvPowerSeries.expand_substAlgHom, IntermediateField.coe_inclusion, CliffordAlgebra.ofBaseChange_toBaseChange, PowerSeries.support_expand_subset, Polynomial.aevalTower_algebraMap, Polynomial.rootsExpandPowEquivRoots_apply, MvPolynomial.map_expand, Polynomial.Bivariate.swap_apply, MvPolynomial.map_aeval, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, MvPolynomial.map_frobenius_expand, LindemannWeierstrass.exp_polynomial_approx, StandardEtalePair.homEquiv_apply_coe, Polynomial.map_expand, AlgCat.forget_map, MvPolynomial.expand_monomial, MvPowerSeries.substAlgHom_eq_aeval, AlgEquiv.arrowCongr_apply, MvPolynomial.expand_char, ExteriorAlgebra.lift_Îč_apply, MvPolynomial.map_rename, MvPowerSeries.hasSum_aeval, MvPolynomial.killCompl_C, MvPolynomial.eval_comp_toMvPolynomial, Algebra.Generators.map_toComp_ker, Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply, Complex.liftAux_apply, PowerSeries.support_expand, CliffordAlgebra.star_def', NonUnitalSubalgebra.unitization_injective, Localization.exists_finite_awayMapâ_of_surjective_awayMapâ, Polynomial.expand_eq_comp_X_pow, TensorAlgebra.toDirectSum_ofDirectSum, CommAlgCat.forgetâ_algCat_map, MvPolynomial.aevalTower_toAlgHom, IntermediateField.aeval_coe, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, CliffordAlgebra.Îč_comp_lift, AdicCompletion.factor_eval_eq_evalâ, Subalgebra.range_isScalarTower_toAlgHom, Normal.algHomEquivAut_symm_apply, CliffordAlgebra.lift_unique, FractionalIdeal.mem_map, Ideal.Quotient.factorâ_apply, Polynomial.aeval_one, Algebra.Extension.CotangentSpace.map_tmul, Polynomial.aevalAeval_X, Polynomial.aeval_eq_zero_of_mem_rootSet, Unitization.lift_symm_apply_apply, IsFractionRing.coe_liftAlgHom, MvPolynomial.coeff_expand_smul, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, Algebra.Generators.algebraMap_apply, RingHom.toIntAlgHom_apply, MonoidAlgebra.mapAlgHom_single, Field.Emb.Cardinal.succEquiv_coherence, Algebra.discr_powerBasis_eq_norm, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, QuaternionAlgebra.Basis.j_compHom, WeierstrassCurve.baseChange_preΚ', IsSepClosed.lift_def, Polynomial.expand_one, MvPolynomial.expand_C, Algebra.toRingHom_ofId, WeierstrassCurve.Affine.baseChange_negY, TensorAlgebra.toExterior_Îč, coe_galRestrict_apply, DoubleQuot.quotQuotToQuotSupâ_toRingHom, Polynomial.aeval_subalgebra_coe, AlgebraicIndependent.map', MvPowerSeries.coeff_embDomain_rename, Polynomial.separable_or, Algebra.TensorProduct.includeLeft_apply, AdjoinRoot.algHomOfDvd_root, Ideal.Fiber.lift_residueField_surjective, Algebra.leftMulMatrix_injective, isConjRoot_iff_aeval_eq_zero, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, Polynomial.aeval_X_left_apply, MvPolynomial.rename_psum, spectrum.gelfandTransform_eq, Algebra.Generators.map_ofComp_ker, BoundedContinuousFunction.charAlgHom_apply, IsLocalization.mapâ_injective_of_injective, CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd, WeierstrassCurve.baseChange_Ïâ, SkewMonoidAlgebra.lift_of, Complex.lift_apply, SkewMonoidAlgebra.lift_single, Subalgebra.inclusion_inclusion, AlgCat.id_apply, MonoidAlgebra.mapRangeAlgHom_single, Polynomial.coeff_mapAlgHom_apply, Polynomial.aeval_prod_apply, SkewMonoidAlgebra.lift_apply, CliffordAlgebra.reverse_involute, IsLocalization.coe_liftAlgHom, Polynomial.aeval_add_of_sq_eq_zero, MvPolynomial.totalDegree_rename_le, Polynomial.Chebyshev.aeval_T, Polynomial.aeval_comp, Polynomial.deriv_aeval, MvPolynomial.coe_mapEquivMonic_comp', CliffordAlgebra.star_def, ExteriorAlgebra.lift_comp_Îč, AddMonoidAlgebra.decomposeAux_coe, Polynomial.monic_mapAlg_iff, CommAlgCat.algEquivOfIso_apply, WeierstrassCurve.Projective.baseChange_polynomial, StarAlgHom.coe_mk', AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, UniversalEnvelopingAlgebra.Îč_comp_lift, AlgHom.opComm_symm_apply_apply, WeierstrassCurve.Affine.baseChange_negPolynomial, Derivation.comp_aeval_eq, Polynomial.aeval_homogenize_X_one, Ideal.kerLiftAlg_injective, Algebra.norm_eq_prod_embeddings, AlgCat.forgetâRing_preservesLimitsOfSize, CliffordAlgebra.involute_mem_evenOdd_iff, AlgHom.coe_restrictScalars, MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, ContinuousMap.coeFnAlgHom_apply, AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, Polynomial.ofReal_eval, Ideal.map_includeRight_eq, Algebra.TensorProduct.includeLeft_bijective, MvPolynomial.transcendental_polynomial_aeval_X_iff, AlgebraicGeometry.pullbackSpecIso_inv_snd, MvPolynomial.aeval_algebraMap_eq_zero_iff_of_injective, AdicCompletion.mkâ_apply_coe, Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProduct, Algebra.Generators.algebraMap_eq, Polynomial.rootsExpandEquivRoots_apply, Field.primitive_element_iff_algHom_eq_of_eval', AdjoinRoot.coe_mapAlgHom, NonUnitalSubsemiring.unitization_apply, PowerBasis.leftMulMatrix, MonoidAlgebra.toRingHom_mapRangeAlgHom, CategoryTheory.Iso.toAlgEquiv_symm_apply, linearIndependent_algHom_toLinearMap', MvPolynomial.support_rename_of_injective, isIntegral_algHom_iff, MonoidAlgebra.scalarTensorEquiv_tmul, Polynomial.algEquivOfTranscendental_coe, MvPolynomial.ACounit_C, Polynomial.expand_C, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, CommAlgCat.algEquivOfIso_symm_apply, Polynomial.aevalTower_toAlgHom, AlgHom.comp_apply, IsAdjoinRootMonic.map_modByMonic, AdjoinRoot.coe_liftHom, MvPolynomial.algebraicIndependent_polynomial_aeval_X, PowerSeries.substAlgHom_X, AlgHom.coe_mk', CommBialgCat.forgetâ_commAlgCat_obj, MvPowerSeries.expand_one_apply, Polynomial.CAlgHom_apply, MvPolynomial.degreeOf_rename_of_injective, GradedTensorProduct.includeLeft_apply, WeierstrassCurve.Projective.baseChange_dblXYZ, Polynomial.toAddCircle.integrable, MvPolynomial.exists_rename_eq_of_vars_subset_range, MvPolynomial.optionEquivRight_symm_apply, PowerSeries.heval_apply, FreeAlgebra.liftAux_eq, spinGroup.units_involute_act_eq_conjAct, IsLocalization.liftAlgHom_apply, TensorAlgebra.lift_symm_apply, Algebra.TensorProduct.map_ker, AddMonoidAlgebra.tensorEquiv.invFun_tmul, PowerSeries.expand_one_apply, WeierstrassCurve.Jacobian.baseChange_nonsingular, Algebra.Generators.Hom.aeval_val, NonUnitalSubring.unitization_apply, Algebra.TensorProduct.productMap_left_apply, Algebra.TensorProduct.algebraMap_eq_includeRight, Polynomial.aeval_pi_apply, IsAdjoinRoot.map_repr, Polynomial.aevalTower_comp_algebraMap, MvPowerSeries.rename_rename, AlgHom.prodEquiv_symm_apply, TensorAlgebra.equivDirectSum_apply, Algebra.Presentation.comp_aeval_relation_inl, IntermediateField.exists_algHom_of_splits', AdjoinRoot.aeval_eq_of_algebra, RatFunc.laurent_at_zero, WittVector.mulN_coeff, Matrix.isRepresentation.toEnd_represents, AlgHom.toRingHom_toOpposite, DualNumber.lift_inlAlgHom_eps, Polynomial.evalâAlgHom_apply, StandardEtalePair.HasMap.map, BialgHom.coe_toAlgHom, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, QuadraticAlgebra.lift_apply_apply, Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans, MvPolynomial.support_expand_subset, QuaternionAlgebra.Basis.k_compHom, Polynomial.aevalTower_X, Algebra.TensorProduct.productMap_apply_tmul, CliffordAlgebra.coe_toEven_reverse_involute, Polynomial.differentiable_aeval, map_mem_perfectClosure_iff, ExteriorAlgebra.Îč_comp_lift, Unitization.splitMul_injective_of_clm_mul_injective, Polynomial.roots_expand_map_frobenius, MvPolynomial.coeff_rename_embDomain, Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral, AlgHom.coe_tensorEqualizer, charpoly_leftMulMatrix, WeierstrassCurve.Jacobian.baseChange_addX, Polynomial.map_under_lt_comap_of_weaklyQuasiFiniteAt, TensorProduct.toIntegralClosure_mvPolynomial_bijective, SubalgebraClass.coe_val, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst, spinGroup.involute_act_Îč_mem_range_Îč, PowerSeries.substAlgHom_comp_substAlgHom, SkewMonoidAlgebra.lift_unique, MvPolynomial.rename_esymm, Polynomial.roots_expand_image_frobenius, AlgHom.coe_prod, Algebra.TensorProduct.lmul'_apply_tmul, linearIndependent_algHom_toLinearMap, TensorAlgebra.lift_Îč_apply, MvPowerSeries.HasSubst.comp, AddMonoidAlgebra.lift_apply, linearIndependent_toLinearMap, minpoly.dvd_iff, Algebra.TensorProduct.includeLeft_injective, AlgHom.toLinearMap_apply, galLift_algebraMap_apply, MvPowerSeries.rename_C, Algebra.Generators.toAlgHom_ofComp_surjective, AlgHom.comap_ker, AlgHom.toNonUnitalAlgHom_eq_coe, MvPolynomial.bindâ_comp_bindâ, Algebra.Generators.Hom.algebraMap_toAlgHom', Subalgebra.iSupLift_mk, LocallyConstant.mapâ_apply_apply, Algebra.Generators.cotangentSpaceBasis_repr_tmul, Polynomial.aevalTower_C, RatFunc.laurent_laurent, MvPolynomial.aevalTower_X, NonUnitalAlgHom.toAlgHom_zero, cfc_map_polynomial, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, FreeAlgebra.lift_Îč_apply, Algebra.pushoutDesc_right, AlgHom.coe_toMonoidHom, ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf, IntermediateField.adjoin_map, exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range, CommAlgCat.lift_unop_hom, RingCon.kerLiftâ_mk, AlgHom.map_adjugate, map_mem_separableClosure_iff, IntermediateField.exists_algHom_adjoin_of_splits_of_aeval, Algebra.FormallySmooth.exists_mkâ_comp_eq_of_isAdicComplete, MvPolynomial.aeval_expand, MvPowerSeries.rename_monomial, DirectSum.toAlgebra_apply, liftOfDerivationToSquareZero_mk_apply, AlgHom.ofLinearMap_apply, AlgebraicIndependent.lift_reprField, DualNumber.lift_smul, MvPolynomial.aeval_algebraMap_apply, IsAdjoinRoot.map_X, gelfandTransform_map_star, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, polynomialFunctions.starClosure_eq_adjoin_X, Algebra.FiniteType.baseChangeAux_surj, LinearMap.pow_eq_aeval_mod_charpoly, Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective, MonoidAlgebra.mapRangeAlgHom_apply, LinearMap.tensorProductEnd_apply, PowerBasis.liftEquiv_symm_apply, LieRinehartAlgebra.Hom.map_smul_apply', Algebra.Generators.H1Cotangent.ÎŽAux_toAlgHom, WeierstrassCurve.Jacobian.baseChange_equation, AlgHom.opComm_apply_apply, CliffordAlgebraComplex.ofComplex_I, PowerSeries.rescale_algebraMap_map, AlgHom.IsArithFrobAt.localize_algebraMap, AlgHom.ker_rangeRestrict, AlgEquiv.ofAlgHom_symm_apply, Subalgebra.mvPolynomial_aeval_coe, RatFunc.Luroth.algEquiv_algebraMap, BialgHom.coe_algHom_injective, Polynomial.rootsExpandPowToRoots_apply, WeierstrassCurve.Projective.baseChange_addXYZ, TensorAlgebra.toClifford_Îč, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, FiniteField.frobeniusAlgEquiv_symm_apply, AdjoinRoot.Minpoly.coe_toAdjoin, PowerSeries.expand_smul, ContinuousMap.compStarAlgHom_comp, CliffordAlgebraQuaternion.equiv_apply, Module.End.rTensorAlgHom_apply_apply, WeierstrassCurve.Jacobian.baseChange_addXYZ, IntermediateField.toSubfield_map, Polynomial.aevalAeval_Y, LocallyConstant.constâ_apply_apply, PowerBasis.equivAdjoinSimple_aeval, PolynomialLaw.exists_lift, Normal.algHomEquivAut_apply, traceForm_dualSubmodule_adjoin, WittVector.mul_polyOfInterest_aux4, AlgCat.forget_preservesLimits, MvPolynomial.rename_evalâ, RingQuot.liftAlgHom_def, AlgHom.IsArithFrobAt.apply_of_pow_eq_one, MvPowerSeries.expand_eq_expand, WeierstrassCurve.baseChange_Ï, MvPowerSeries.substAlgHom_comp_substAlgHom_apply, IsAdjoinRootMonic.modByMonicHom_map, AlgHom.restrictScalars_injective, Polynomial.sup_aeval_range_eq_top_of_isCoprime, Derivation.Compatible.mem, Algebra.FiniteType.iff_quotient_mvPolynomial', Algebra.TensorProduct.includeRight_injective, MvPowerSeries.killCompl_monomial_embDomain, spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots, TensorAlgebra.lift_comp_Îč, BoundedContinuousFunction.AlgHom.compLeftContinuousBounded_apply_apply, Ideal.quotientKerAlgEquivOfRightInverse_symm_apply, StarAlgHom.coe_toAlgHom, CliffordAlgebraQuaternion.equiv_symm_apply, AlgHom.map_det, Polynomial.aevalAevalEquiv_symm_apply_snd, Field.nonempty_algHom_of_exists_root, WeierstrassCurve.Jacobian.baseChange_dblX, AlgHom.mulLeftRight_apply, WeierstrassCurve.Jacobian.baseChange_negDblY, Ideal.mapCotangent_toCotangent, WeierstrassCurve.Jacobian.baseChange_polynomialY, Polynomial.fderiv_aeval, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkâ, CliffordAlgebra.map_apply_Îč, MvPolynomial.evalâHom_rename, CommRingCat.Under.tensorProdEqualizer_Îč, IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zero, Algebra.TensorProduct.lmul'_comp_map, Module.End.aeval_apply_of_hasEigenvector, PowerBasis.mem_span_pow', IsAzumaya.bij, AlgCat.forgetâModule_preservesLimitsOfSize, Algebra.FormallySmooth.mk_lift, WeierstrassCurve.Projective.baseChange_polynomialY, AlgebraicIndependent.aeval_of_algebraicIndependent, AlgHom.toKerIsLocalization_apply, MvPolynomial.aeval_bindâ, Polynomial.isCoprime_expand, CliffordAlgebraQuaternion.ofQuaternion_star, MonoidAlgebra.lift_unique, HomogeneousLocalization.awayMapâ_apply, QuaternionAlgebra.lift_apply, MvPolynomial.killCompl_monomial_eq_zero_of_not_subset, MvPolynomial.exists_fin_rename, AlgHom.mem_range, galLiftEquiv_apply, AdicCompletion.factorâ_evalâ_one, AlgHom.comp_algebraMap_of_tower, Algebra.FiniteType.iff_quotient_freeAlgebra, minpoly.algHom_eq, Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits_apply_apply, Ideal.quotientKerAlgEquivOfRightInverse_apply, AlgHom.mapMatrix_apply, transcendental_aeval_iff, Polynomial.Splits.aeval_eq_prod_aroots, Polynomial.aeval_modByMonic_eq_self_of_root, MonoidAlgebra.lift_apply', AlgEquiv.ofLeftInverse_apply, Polynomial.expand_inj, MvPolynomial.renameEquiv_apply, CliffordAlgebra.comp_Îč_sq_scalar, MvPolynomial.aeval_eq_zero, MvPolynomial.evalâ_cast_comp, IsScalarTower.coe_toAlgHom, CliffordAlgebra.even.lift_Îč, Algebra.embeddingsMatrixReindex_eq_vandermonde, TrivSqZeroExt.lift_apply_inr, AlgHom.IsArithFrobAt.comap_eq, Algebra.adjoin_range_eq_range_freeAlgebra_lift, NumberField.Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm, WeierstrassCurve.Jacobian.baseChange_dblY, Polynomial.aeval_X_left_eq_map, MvPolynomial.bindâ_C_right, AdicCompletion.mk_ofAlgEquiv_symm, Complex.algHom_ext_iff, BialgHom.toAlgHom_toLinearMap, normalClosure_def, MvPolynomial.rename_zero, Polynomial.expand_expand, Subalgebra.mulMap'_surjective, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_auxâ, Polynomial.mapAlgHom_monomial, AlgHom.IsArithFrobAt.restrict_injective, WittVector.bindâ_wittMulN_wittPolynomial, BialgCat.forgetâ_algebra_map, DoubleQuot.coe_quotQuotEquivQuotSupâ, AnalyticWithinAt.aeval_polynomial, Subalgebra.coe_equivMapOfInjective_apply, Subalgebra.mem_map, isConjRoot_algHom_iff_of_injective, sum_embeddings_eq_finrank_mul, MvPolynomial.aevalTower_C, DirectSum.coeAlgHom_of, MvPolynomial.expand_one_apply, IntermediateField.exists_algHom_of_splits, Complex.liftAux_apply_I, MvPolynomial.map_expand_pow_char, MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure, Polynomial.aeval_apply_smul_mem_of_le_comap, AlgEquiv.ofBijective_apply, Pi.algHom_apply, WeakDual.CharacterSpace.toAlgHom_apply, Field.Emb.Cardinal.equivSucc_coherence, FiniteField.frobeniusAlgEquivOfAlgebraic_symm_apply, AlgHom.toLinearMap_injective, minpoly.ker_aeval_eq_span_minpoly, RingCon.factorâ_mk, Polynomial.Chebyshev.aeval_S, AnalyticOnNhd.aeval_mvPolynomial, Polynomial.mem_annIdeal_iff_aeval_eq_zero, MvPowerSeries.coeff_expand_smul, Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, RingQuot.liftAlgHom_mkAlgHom_apply, Matrix.isRepresentation.toEnd_exists_mem_ideal, Representation.asAlgebraHom_single_one, Algebra.Generators.Hom.toAlgHom_X, MvPolynomial.bindâ_rename, Polynomial.scaleRoots_aeval_eq_zero, MvPowerSeries.rename_id_apply, Polynomial.mapAlg_eq_map, ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply, wittStructureRat_prop, IsPrimitiveRoot.minpoly_dvd_expand, Algebra.TensorProduct.congr_apply, Polynomial.eval_unique, MvPolynomial.degrees_rename, Algebra.Presentation.comp_relation, MvPowerSeries.aeval_coe, Polynomial.aeval_eq_smeval, WittVector.IsPoly.poly, AdicCompletion.kerProj_surjective, WeierstrassCurve.baseChange_Ί, Algebra.adjoin_mem_exists_aeval, AlgHom.fst_apply, QuaternionAlgebra.Basis.liftHom_apply, wittStructureRat_rec, HahnSeries.embDomainAlgHom_apply_coeff, IntermediateField.coe_val, MvPolynomial.expand_eq_C, Polynomial.roots_expand_image_frobenius_subset, RingQuot.liftAlgHom_unique, Polynomial.isNilpotent_aeval_sub_of_isNilpotent_sub, Module.End.IsSemisimple.aeval, MvPowerSeries.trunc'_expand, AlgHom.fieldRange_toSubfield, MvPolynomial.coeff_rename_mapDomain, StandardEtalePair.lift_X, Algebra.lsmul_injective, LocallyConstant.coeFnAlgHom_apply, Localization.localAlgHom_apply, MvPolynomial.expand_injective, minpoly.aeval, Algebra.Presentation.aeval_val_relation, MonoidAlgebra.isLocalHom_singleOneAlgHom, TrivSqZeroExt.liftEquiv_apply, QuaternionAlgebra.Basis.i_compHom, MvPolynomial.esymmAlgHom_fin_surjective, MvPolynomial.expand_inj, AlgHom.mul_apply, GradedAlgHom.coe_comp, MvPowerSeries.comp_subst_apply, Algebra.TensorProduct.includeRight_bijective, UniversalEnvelopingAlgebra.lift_Îč_apply, MvPowerSeries.rename_coe, Algebra.Generators.H1Cotangent.ÎŽAux_ofComp, QuaternionAlgebra.lift_symm_apply, TrivSqZeroExt.inlAlgHom_apply, Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, MvPolynomial.killCompl_monomial_mapDomain, WeierstrassCurve.Projective.baseChange_equation, AlgHom.one_apply, PiTensorProduct.singleAlgHom_apply, Polynomial.int_evalâ_eq, AdjoinRoot.liftAlgHom_eq_algHom, Submodule.LinearDisjoint.map, CommRingCat.toAlgHom_apply, WeierstrassCurve.Jacobian.baseChange_dblU, Algebra.TensorProduct.liftEquiv_apply, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply, exists_integral_inj_algHom_of_quotient, padic_polynomial_dist, Localization.mapToFractionRing_apply, TensorAlgebra.ofDirectSum_toDirectSum, Polynomial.aeval_conj, FreeAlgebra.toTensor_Îč, CategoryTheory.Iso.toAlgEquiv_apply, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, Matrix.scalarAlgHom_apply, exists_finite_inj_algHom_of_fg, AlgHom.default_apply, Polynomial.algEquivAevalNegX_symm_apply, Field.nonempty_algHom_of_range_minpoly_subset, ExteriorAlgebra.map_apply_Îč, WeierstrassCurve.Jacobian.baseChange_polynomial, IsAdjoinRoot.adjoinRootAlgEquiv_apply_eq_map, MvPolynomial.aeval_def, Polynomial.hermite_eq_deriv_gaussian', Polynomial.Splits.image_rootSet, Polynomial.aeval_smul, CliffordAlgebra.involute_eq_of_mem_even, BialgHom.ofAlgHom_apply, AddMonoidAlgebra.lift_single, AlgHom.natCard_of_splits, AlgebraicIndependent.map, GradedTensorProduct.includeRight_apply, Algebra.FormallyUnramified.comp_injective, CliffordAlgebra.ofBaseChange_tmul_Îč, Algebra.Generators.toAlgHom_ofComp_rename, AddMonoidAlgebra.mapDomainAlgHom_apply, wittStructureRat_rec_aux, Algebra.algebraMapSubmonoid_map_eq, PowerBasis.mem_span_pow, Polynomial.aeval_def, galLiftEquiv_symm_apply, AlgHom.IsArithFrobAt.le_comap, Polynomial.aeval_mul, MvPolynomial.totalDegree_expand, AlgHom.map_adjoin, MvPolynomial.algHom_C, RatFunc.minpolyX_aeval_X, AlgHom.card_of_powerBasis, AddMonoidAlgebra.lift_symm_apply, RatFunc.algEquivOfTranscendental_symm_aeval, StandardEtalePresentation.toSubmersivePresentation_jacobian, IsAlgClosed.exists_aeval_eq_zero_of_injective, Algebra.IsAlgebraic.algHom_bijectiveâ, wittStructureInt_prop, Algebra.pushoutDesc_apply, Polynomial.expand_eq_zero, Polynomial.algEquivOfTranscendental_apply, Polynomial.differentiableAt_aeval, WeakDual.CharacterSpace.compContinuousMap_apply, Submodule.coe_mulMap_comp_eq, AdjoinRoot.mapAlgHom_comp_mapAlghom, Ideal.kerLiftAlg_toRingHom, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, Polynomial.taylorAlgHom_apply, Subalgebra.inclusion_mk, RingCon.kerLiftâ_injective, DoubleQuot.coe_quotQuotEquivQuotSupâ_symm, CommAlgCat.hom_inv_apply, Polynomial.hasFDerivAt_aeval, IsAdjoinRoot.lift_map, Subalgebra.inclusion_injective, Polynomial.algEquivOfCompEqX_symm_apply, CliffordAlgebra.ofBaseChangeAux_Îč, Unitization.lift_range, Derivation.Compatible.apply, Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splits, AlgHom.compLeft_apply, Polynomial.eval_X_toTupleMvPolynomial_zero_eq, AdjoinRoot.liftAlgHom_mk, AlgHom.snd_apply, LinearMap.aeval_eq_aeval_mod_charpoly, AlgHom.range_eq_top, Polynomial.deriv_gaussian_eq_hermite_mul_gaussian, Algebra.Generators.comp_localizationAway_ker, Polynomial.algEquivAevalXAddC_symm_apply, MvPolynomial.rename_monomial, MvPolynomial.aeval_toMvPolynomial, derivationToSquareZeroEquivLift_symm_apply_apply_coe, AdjoinRoot.coe_mkâ, Differential.deriv_aeval_eq_implicitDeriv, Algebra.smulTower_leftMulMatrix, CliffordAlgebra.lift_symm_apply, MvPowerSeries.expand_subst, IsLocalization.integerNormalization_aeval_eq_zero, Module.Finite.exists_free_surjective, galRestrictHom_symm_algebraMap_apply, MvPolynomial.universalFactorizationMapPresentation_relation, AnalyticAt.aeval_polynomial, MonoidAlgebra.mapAlgHom_apply, MvPolynomial.aevalTower_comp_algebraMap, Ideal.quotientKerAlgEquivOfSurjective_apply, QuadraticAlgebra.lift_symm_apply_coe, DoubleQuot.quotQuotMkâ_toRingHom, Polynomial.Monic.mem_rootSet, Algebra.PreSubmersivePresentation.aevalDifferential_single, AlgebraicIndependent.algebraMap_aevalEquiv, spectrum.map_polynomial_aeval_of_nonempty, UniversalEnvelopingAlgebra.lift_symm_apply, AdjoinRoot.Minpoly.coe_toAdjoin_mk_X, MvPolynomial.aeval_id_rename, MvPowerSeries.killCompl_rename_app, Polynomial.expand_zero, CliffordAlgebraQuaternion.ofQuaternion_mk, WeierstrassCurve.Projective.baseChange_dblZ, Polynomial.roots_expand_pow_map_iterateFrobenius_le, AddMonoidAlgebra.mapAlgHom_apply, AddMonoidAlgebra.coe_liftNCAlgHom, TensorProduct.toIntegralClosure_bijective_of_tower, PowerBasis.equivOfMinpoly_aeval, MvPowerSeries.rename_inj, MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero, Algebra.Generators.aeval_val_Ï, Subalgebra.algebraMap_eq, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkâ, Algebra.TensorProduct.map_surjective, MvPolynomial.mem_zeroLocus_iff, Polynomial.rootMultiplicity_expand, NonUnitalSubalgebra.unitization_apply, AlgHom.tensorEqualizerEquiv_apply, DualNumber.lift_apply_apply, AlgEquiv.coe_algHom_injective, AlgHom.liftOfSurjective_surjective, Algebra.ofId_apply, WeierstrassCurve.Affine.baseChange_addPolynomial, AlgEquiv.arrowCongr_comp, Unitization.lift_symm_apply, AlgHom.fromOpposite_apply, transcendental_iff_ker_eq_bot, MonoidAlgebra.tensorEquiv_tmul, Algebra.FormallySmooth.exists_lift, MvPolynomial.aeval_eq_constantCoeff_of_vars, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, SymmetricAlgebra.algHom_ext_iff, AddMonoidAlgebra.lift_of, ExteriorAlgebra.toTrivSqZeroExt_Îč, Polynomial.expand_X, Ideal.Quotient.mkâ_ker, MvPolynomial.expand_bindâ, CliffordAlgebra.toBaseChange_ofBaseChange, minpoly.isIntegrallyClosed_dvd_iff, SkewMonoidAlgebra.lift_unique', CliffordAlgebraComplex.equiv_symm_apply, Polynomial.expand_monomial, AlgHom.liftOfSurjective_apply, MvPowerSeries.substAlgHom_coe, GradedAlgHom.toEnd_apply, RingCon.quotientQuotientEquivQuotientâ_mk_mk, CliffordAlgebra.evenToNeg_Îč, MvPolynomial.coeff_rTensorAlgHom_tmul, FiniteGaloisIntermediateField.adjoin_map, Representation.asAlgebraHom_of, MvPolynomial.aeval_zero, WeierstrassCurve.baseChange_Κ, Algebra.leftMulMatrix_complex, RingHom.equivRatAlgHom_apply, MvPolynomial.killCompl_rename_app, diffToIdealOfQuotientCompEq_apply, AlgEquiv.algHomUnitsEquiv_apply_symm_apply, MvPolynomial.comp_aeval, CliffordAlgebra.commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_left, Polynomial.image_rootSet, MvPolynomial.frobenius_zmod, Subalgebra.comap_toSubsemiring, PowerSeries.expand_C, LinearMap.prodMapAlgHom_apply_apply, Polynomial.hermite_eq_deriv_gaussian, MvPowerSeries.killCompl_map, IntermediateField.mem_adjoin_range_iff, RatFunc.liftAlgHom_apply_div, Algebra.FormallySmooth.liftOfSurjective_apply, CommAlgCat.forgetâ_algCat_obj, SymmetricAlgebra.lift_comp_Îč, DividedPowerAlgebra.mkAlgHom_surjective, AlgEquiv.coe_ofBijective, WittVector.coeff_frobeniusFun, AlgEquiv.val_algHomUnitsEquiv_symm_apply, SymmetricAlgebra.lift_Îč, Algebra.adjoin_eq_exists_aeval, QuaternionAlgebra.hom_ext_iff, Algebra.toMatrix_lmul', MvPolynomial.expand_mul, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, WeierstrassCurve.Projective.baseChange_polynomialX, MvPolynomial.isLocalHom_expand, ExteriorAlgebra.map_injective_field, Unitization.norm_def, Polynomial.mem_roots_iff_aeval_eq_zero, WeierstrassCurve.Affine.baseChange_polynomialX, FreeAlgebra.Îč_comp_lift, CliffordAlgebraComplex.toComplex_Îč, AdjoinRoot.toRingHom_liftAlgHom, WeierstrassCurve.Jacobian.baseChange_neg, Polynomial.hasDerivWithinAt_aeval, RingCon.coe_comapQuotientEquivRangeâ_symm_mk, IntermediateField.card_algHom_adjoin_integral, Polynomial.aeval_coe_eq_smeval, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, Polynomial.IsMonicOfDegree.aeval_add, Algebra.FormallySmooth.comp_surjective, AlgebraicClosure.toSplittingField_coeff, Polynomial.hasStrictDerivAt_aeval, Algebra.embeddingsMatrix_apply, RestrictScalars.lsmul_apply_apply, Subalgebra.coe_val, Polynomial.aeval_algebraMap_eq_zero_iff_of_injective, AlgHom.toUnder_right, StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x, AlgHom.liftNormal_commutes, ExteriorAlgebra.map_injective, AlgHom.coe_mks, CommAlgCat.forget_obj, IsAdicComplete.mk_liftAlgHom, Algebra.FormallyEtale.iff_comp_bijective, LinearAlgebra.FreeProduct.lift_unique, MvPowerSeries.expand_comp_substAlgHom, DualNumber.coe_lift_symm_apply, Algebra.TensorProduct.algEquivIncludeRange_tmul, PowerSeries.subst_coe, MatrixEquivTensor.left_inv, Subalgebra.iSupLift_of_mem, Algebra.smulTower_leftMulMatrix_algebraMap_ne, minpoly.aeval_algHom, Algebra.adjoin_image, AlgHom.coe_comp, TrivSqZeroExt.liftEquivOfComm_apply, Subalgebra.coe_map, Polynomial.monic_expand_iff, Polynomial.natSepDegree_expand, Algebra.Extension.ofSurjective_Ï, AlgHom.toRingHom_fromOpposite, Polynomial.toAddCircle_monomial_eq_smul_fourier, CliffordAlgebra.toBaseChange_comp_reverseOp, Polynomial.aeval_apply_smul_mem_of_le_comap', algebraicIndependent_iff_injective_aeval, MvPolynomial.aeval_map_algebraMap, Algebra.Generators.Hom.toAlgHom_C, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, AlgHom.coe_fieldRange, Subalgebra.LinearDisjoint.linearIndependent_right_of_flat, Matrix.diagonalAlgHom_apply, Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt, Algebra.smul_units_def, DoubleQuot.coe_quotQuotEquivQuotOfLEâ, AlgHom.congr_arg, MvPolynomial.coeToMvPowerSeries.algHom_apply, IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk, AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc, Polynomial.scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero, AlgebraicIndependent.liftAlgHom_comp_reprField, AlgCat.forgetâ_module_obj, DividedPowerAlgebra.algHom_ext_iff, sectionOfRetractionKerToTensor_algebraMap, MvPolynomial.rename_rightInverse, exists_leadingCoeff_pow_smul_mem_radical_conductor, RingCon.mkâ_apply, LinearMap.aeval_self_charpoly, WeierstrassCurve.Projective.baseChange_add, Polynomial.rootSet_maps_to', AlgHom.coe_ideal_map, AlgHom.coe_restrictScalars', RingCon.comapQuotientEquivRangeâ_mk, Differential.algHom_deriv', RatFunc.liftAlgHom_apply_ofFractionRing_mk, AlgEquiv.coe_algHom, SkewMonoidAlgebra.mapDomainAlgHom_apply, AddMonoidAlgebra.lift_unique', LinearMap.polyCharpoly_eq_of_basis, RingCon.factorâ_apply, Algebra.discr_powerBasis_eq_prod, spectrum.subset_polynomial_aeval, PowerSeries.expand_mul, MvPolynomial.ker_evalâHom_universalFactorizationMap, PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul, Ideal.constr_basisSpanSingleton, IsAdjoinRootMonic.map_modByMonicHom, TensorProduct.toIntegralClosure_bijective_of_isLocalizationAway, AdjoinRoot.toRingHom_ofAlgHom, Algebra.trace_eq_matrix_trace, IsConjRoot.aeval_eq_zero, Polynomial.Bivariate.aevalAeval_swap, MvPolynomial.evalâ_rename, AlgebraicIndependent.aeval_repr, MvPolynomial.support_expand, AdjoinRoot.liftHom_eq_algHom, AdicCompletion.kerProj_of, IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen, AddMonoidAlgebra.tensorEquiv_tmul, Algebra.FiniteType.iff_quotient_freeAlgebra', PolyEquivTensor.toFunBilinear_apply_apply, MvPolynomial.IsSymmetric.rename, MvPolynomial.IsHomogeneous.aeval, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, RatFunc.laurent_C, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, Module.AEval.mem_mapSubmodule_symm_apply, RingHom.toNatAlgHom_coe, StandardEtalePresentation.lift_bijective, Polynomial.aeval_eq_aeval_map, UniversalEnvelopingAlgebra.Îč_apply, Polynomial.algHom_ext_iff, Polynomial.coeToPowerSeries.algHom_apply, AdicCompletion.evalOneâ_of, PowerBasis.equivOfMinpoly_apply, GradedAlgHom.coe_toAlgHom, CommAlgCat.forget_map, WeierstrassCurve.map_baseChange, Algebra.FormallySmooth.iff_split_surjection, AlgHom.eqOn_adjoin_iff, Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C, AlgHom.map_smul_of_tower, CliffordAlgebra.prodEquiv_symm_apply, MvPowerSeries.expand_monomial, MvPolynomial.aeval_bindâ, MvPolynomial.rename_bindâ, AlgHom.card, RingCon.mkâ_surjective, MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe, StandardEtalePair.hom_ext_iff, Algebra.Generators.Hom.toAlgHom_comp_apply, Polynomial.roots_expand_pow_map_iterateFrobenius, MvPowerSeries.order_expand, WeierstrassCurve.Affine.baseChange_equation, Polynomial.map_expand_pow_char, IsAdjoinRoot.liftHom_map, CliffordAlgebra.involute_Îč, IsPurelyInseparable.bijective_restrictDomain, bindâ_rename_expand_wittPolynomial, HahnSeries.ofPowerSeriesAlg_apply_coeff, Algebra.Generators.toComp_toAlgHom_monomial, WeierstrassCurve.Affine.baseChange_polynomial, Polynomial.coeff_expand_mul, MvPowerSeries.map_iterateFrobenius_expand, RingCon.quotientQuotientEquivQuotientâ_symm_mk, MvPolynomial.rename_injective, IntermediateField.inclusion_injective, Subalgebra.mem_comap, TensorAlgebra.range_lift, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, AlgHom.algebraicIndependent_iff, not_irreducible_expand, AddMonoidAlgebra.lift_of', liftOfDerivationToSquareZero_apply, Derivation.tensorProductTo_mul, AlgHom.fieldRange_eq_top, TrivSqZeroExt.lift_def, AdjoinRoot.equiv'_symm_apply, Polynomial.expand_mul, MvPolynomial.killCompl_map, Algebra.IsAlgebraic.bijective_of_isScalarTower', Polynomial.aeval_continuousMap_apply, Polynomial.coe_aeval_mk_apply, PowerSeries.heval_X, Algebra.FiniteType.iff_quotient_mvPolynomial, AdjoinRoot.coe_liftAlgHom, FreeAlgebra.lift_unique, AlgHom.subalgebraMap_coe_apply, WeierstrassCurve.Jacobian.baseChange_dblXYZ, Polynomial.coeff_zero_eq_aeval_zero, CliffordAlgebra.prodEquiv_apply, Algebra.TensorProduct.tensorQuotientEquiv_symm_apply_tmul, MvPowerSeries.constantCoeff_rename, AlgHom.card_le, Polynomial.existsUnique_nilpotent_sub_and_aeval_eq_zero, MvPolynomial.aeval_ofNat, CliffordAlgebra.involute_involute, Algebra.smulTower_leftMulMatrix_algebraMap, Algebra.Presentation.aeval_val_relationOfHasCoeffs, cfc_polynomial, WeierstrassCurve.baseChange_Ï, polynomial_expand_eq, MvPolynomial.expand_comp_bindâ, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, MvPolynomial.ker_mapAlgHom, MvPolynomial.aeval_injective_iff_of_isEmpty, galRestrict_apply, Algebra.Generators.ofComp_kerCompPreimage, IntermediateField.LinearDisjoint.linearIndependent_right, Unitization.fstHom_apply, AlgHom.coe_toContinuousLinearMap, AlgHomClass.toLinearMap_toAlgHom, CliffordAlgebra.involuteEquiv_apply, MvPolynomial.esymmAlgHom_fin_injective, Polynomial.coe_expand, MvPolynomial.aeval_comp_bindâ, WeierstrassCurve.Projective.baseChange_addX, ExteriorAlgebra.map_surjective_iff, polynomialFunctions_coe, CliffordAlgebra.even.lift_symm_apply_bilin, CliffordAlgebra.evenEquivEvenNeg_apply, Polynomial.fourierCoeff_toAddCircle_natCast, Subalgebra.linearDisjoint_iff_injective, QuadraticAlgebra.algHom_ext_iff, spectrum.map_polynomial_aeval_of_degree_pos, scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero, AlgHom.mem_fieldRange, Algebra.Generators.repr_CotangentSpaceMap, MonoidAlgebra.lift_apply, Polynomial.annIdealGenerator_aeval_eq_zero, Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero, DoubleQuot.quotQuotEquivQuotOfLEâ_comp_mkâ, MonoidAlgebra.lift_mapRangeRingHom_algebraMap, isNilpotent_tensor_residueField_iff, Polynomial.toContinuousMapAlgHom_apply, IsPurelyInseparable.injective_restrictDomain, Polynomial.sup_ker_aeval_le_ker_aeval_mul, Polynomial.fderivWithin_aeval, MvPolynomial.aeval_esymm_eq_multiset_esymm, AlgCat.forget_preservesLimitsOfSize, CliffordAlgebraComplex.equiv_apply, BialgCat.MonoidalCategory.inducingFunctorData_ÎŒIso, Ideal.Quotient.mkâ_eq_mk, MvPolynomial.eval_rename, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, FiniteField.nonempty_algHom_extension, StandardEtalePresentation.toPresentation_Ï', AlgHom.toRingHom_eq_coe, witt_structure_prop, Derivation.map_aeval, WeierstrassCurve.Jacobian.Equation.baseChange, CliffordAlgebra.toEven_Îč, AlgHom.adjoin_le_equalizer, Polynomial.Splits.aeval_eq_prod_aroots_of_monic, MvPolynomial.coe_evalâAlgHom, PolyEquivTensor.left_inv, CliffordAlgebra.equivBaseChange_apply, LinearMap.toMvPolynomial_comp, AlgHom.coe_toLieHom, WeierstrassCurve.Jacobian.baseChange_dblZ, Complex.lift_symm_apply_coe, MvPowerSeries.coeff_expand_of_not_dvd, FreeAlgebra.lift_symm_apply, MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff, Polynomial.aeval_neg, MvPolynomial.vars_bindâ, WittVector.bindâ_verschiebungPoly_wittPolynomial, aeval_derivative_mem_differentIdeal, AddMonoidAlgebra.lift_mapRingHom_algebraMap, PowerSeries.map_expand, AlgHom.algebraMap_eq_apply, AdicCompletion.evalâ_liftAlgHom, AdicCompletion.surjective_evalâ, MvPowerSeries.rescaleAlgHom_apply, DualNumber.algHom_ext_iff, Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map, MvPolynomial.optionEquivRight_apply, Polynomial.coeff_expand, AlgCat.free_map, Polynomial.rootsExpandToRoots_apply, RingQuot.mkAlgHom_rel, StandardEtalePair.HasMap.isUnit_derivative_f, Polynomial.isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub, Polynomial.leadingCoeff_expand, MvPolynomial.comp_aeval_apply, Algebra.Presentation.relation_comp_localizationAway_inl, Polynomial.aeval_sumIDeriv_eq_eval, WittVector.coeff_select, PowerSeries.coeff_expand_of_not_dvd, Subalgebra.coe_comap, AlgEquiv.arrowCongr_trans, Polynomial.expand_eq_C, MvPolynomial.aeval_unique, WeierstrassCurve.Jacobian.baseChange_polynomialX, AlgEquiv.toAlgHom_unop, Polynomial.aeval_C, PowerBasis.exists_eq_aeval', Algebra.toMatrix_lsmul, DividedPowerAlgebra.dp_def, Polynomial.aeval_eq_prod_aroots_sub_of_splits, MvPolynomial.coeff_rTensorAlgHom_monomial_tmul, MvPolynomial.bindâ_bindâ, TensorProduct.toIntegralClosure_injective_of_flat, Polynomial.newtonMap_apply_of_isUnit, Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime, AdicCompletion.mk_ofAlgEquiv_symm_eq_evalOneâ, Algebra.TensorProduct.productMap_right_apply, exists_derivative_mul_eq_and_isIntegral_coeff, Module.End.baseChangeHom_apply_apply, MvPolynomial.rename_polynomial_aeval_X, MvPolynomial.coeff_expand_of_not_dvd, Matrix.isRepresentation.toEnd_surjective, IntermediateField.exists_algHom_adjoin_of_splits', Polynomial.comp_eq_aeval, FixedPoints.toAlgHom_bijective, Algebra.Generators.Hom.equivAlgHom_symm_apply_val, Polynomial.valuation_aeval_monomial_eq_valuation_pow, AlgHom.toRingHom_unop, MvPolynomial.map_iterateFrobenius_expand, Polynomial.toMvPolynomial_X, FiniteField.natCard_algHom_of_finrank_dvd, MvPowerSeries.coe_aeval, PowerBasis.equivOfRoot_apply, Polynomial.aeval_ofReal, AddMonoidAlgebra.algHom_ext_iff, Algebra.Generators.ker_comp_eq_sup, map_mem_algebraicClosure_iff, AlgHom.natCard_of_powerBasis, Polynomial.hasDerivAt_aeval, WeierstrassCurve.Projective.baseChange_dblX, MvPowerSeries.killCompl_X_eq_zero, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, Polynomial.Chebyshev.aeval_C, Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply, Ideal.quotientKerAlgEquivOfSurjective_symm_apply, Polynomial.aeval_eq_sum_range, polyEquivTensor_apply, MvPolynomial.exists_finset_renameâ, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply, WeierstrassCurve.Projective.baseChange_dblU, MvPolynomial.eval_toMvPolynomial, Ideal.quotientKerAlgEquivOfSurjective_mk, AlgCat.forgetâModule_preservesLimits, Polynomial.aeval_op_apply, Algebra.Generators.aeval_val_eq_zero, Polynomial.Chebyshev.aeval_U, TrivSqZeroExt.snd_map, RingCon.quotientKerEquivRangeâ_mkâ, Submodule.mulMap_map_comp_eq, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, MvPolynomial.esymmAlgHom_apply, AlgHom.addHomMk_coe, MvPolynomial.aeval_eq_evalâHom, DoubleQuot.quotQuotEquivCommâ_toRingEquiv, DoubleQuot.coe_quotQuotToQuotSupâ, MvPowerSeries.rename_injective, MvPolynomial.rename_prod_mk_evalâ, LocallyConstant.evalâ_apply, Differential.deriv_aeval_eq, AlgebraicIndependent.aevalEquivField_apply_coe, MvPolynomial.aeval_C, NonUnitalAlgHom.toAlgHom_apply, Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top, AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply, MvPowerSeries.map_frobenius_expand, IntermediateField.LinearDisjoint.exists_field_of_isDomain, MonoidAlgebra.lift_mapRingHom_algebraMap, MvPolynomial.transcendental_polynomial_aeval_X, WeierstrassCurve.Projective.baseChange_nonsingular, Algebra.TensorProduct.lift_tmul, AdjoinRoot.algHom_subsingleton, AlgebraicIndependent.aevalEquiv_apply_coe, MvPolynomial.rename_C, AlgHom.liftEquiv_tmul, cardinalMk_algHom_le_rank, MvPowerSeries.expand_X, AlgHom.commutes, MvPowerSeries.map_expand, AlgHom.subalgebraMap_surjective, Algebra.Extension.Hom.sub_aux, StandardEtalePresentation.aeval_val_equivMvPolynomial, Ideal.map_mapâ, Module.Basis.localizationLocalization_span, Polynomial.mem_rootSet', AlgHom.congr_fun, PowerSeries.HasSubst.comp, CliffordAlgebra.reverseOp_Îč, MvPowerSeries.killCompl_monomial_eq_zero, AlgHom.bijective, Algebra.TensorProduct.lTensor_ker, AlgHom.map_coe_real_complex, IntermediateField.map_mem_map, MvPolynomial.IsHomogeneous.rename_isHomogeneous, ExteriorAlgebra.algebraMap_leftInverse, Algebra.norm_apply, DoubleQuot.quotQuotEquivQuotSupâ_toRingEquiv, WittVector.polyOfInterest_vars_eq, AlgHom.coe_fn_injective, AlgCat.comp_apply, Algebra.IsAlgebraic.algEquivEquivAlgHom_apply, NormedAlgebra.Real.exists_isMonicOfDegree_two_and_aeval_eq_zero, IsLocalization.mapâ_surjective_of_surjective, AlgHom.End_toOne_one, IsAdjoinRoot.algebraMap_apply, BoundedContinuousFunction.coe_toContinuousMapâ, exists_leadingCoeff_pow_smul_mem_conductor, AlgHom.compLeftContinuous_apply_apply, StandardEtalePair.aeval_X_g_mul_mk_X, MvPolynomial.pderiv_inr_universalFactorizationMap_X, TrivSqZeroExt.fst_map, Transcendental.aeval, MvPowerSeries.constantCoeff_expand, RatFunc.liftAlgHom_apply, Representation.ofModule_asAlgebraHom_apply_apply, TensorAlgebra.equivDirectSum_symm_apply, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, galRestrictHom_symm_apply, PowerSeries.continuous_aeval, derivationOfSectionOfKerSqZero_apply_coe, Algebra.Generators.ker_eq_ker_aeval_val, Polynomial.aeval_endomorphism, FiniteField.bijective_frobeniusAlgHom_pow, IsGalois.of_separable_splitting_field_aux, IntermediateField.coe_equivMap_apply, IntermediateField.mem_adjoin_simple_iff, Matrix.isRepresentation.eq_toEnd_of_represents, PowerSeries.heval_unit, sectionOfRetractionKerToTensorAux_algebraMap, IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe, AlgHom.toRingHom_op, SymmetricAlgebra.algHom_surjective, Algebra.baseChange_lmul, WeakDual.gelfandTransform_apply_apply, Polynomial.expand_contract', Module.AEval.of_aeval_smul, Algebra.mem_ideal_map_adjoin, Polynomial.Bivariate.Transcendental.algEquivAdjoin_apply, Polynomial.mem_aroots, WeierstrassCurve.Affine.Point.map_some, ZMod.expand_card, Polynomial.Bivariate.aeval_aeval_eq_aeval_algEquivAdjoin, MvPolynomial.aeval_C_comp_left, Subalgebra.LinearDisjoint.linearIndependent_left_of_flat_of_commute, IsAdjoinRoot.map_self, Algebra.leftMulMatrix_mulVec_repr, TrivSqZeroExt.liftEquivOfComm_symm_apply_coe, ExteriorAlgebra.map_apply_ÎčMulti, IsLocalization.mapâ_coe, AlgCat.forget_reflects_isos, MvPolynomial.degrees_rename_of_injective, AlgHom.restrictScalars_apply, IsAdjoinRoot.coe_liftHom, LieRinehartAlgebra.Hom.map_smul_apply, PowerBasis.liftEquiv'_apply_coe, MvPolynomial.mapAlgHom_apply, Algebra.Generators.cotangentRestrict_mk, limit_zero_of_norm_tendsto_zero, minpoly.coe_equivAdjoin, Algebra.pushoutDesc_left, Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply, CliffordAlgebra.toProd_one_tmul_Îč, MvPolynomial.rename_eq_zero_iff_of_injective, MvPowerSeries.substAlgHom_monomial, CliffordAlgebra.toBaseChange_involute, Polynomial.aevalEquiv_symm_apply, Polynomial.algEquivAevalNegX_apply, WittVector.bindâ_onePoly_wittPolynomial, Algebra.adjoin_eq_range_freeAlgebra_lift, Module.End.ker_aeval_ring_hom'_unit_polynomial, Algebra.lmul_isUnit_iff, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, MvPolynomial.optionEquivLeft_symm_apply, Polynomial.hasFDerivWithinAt_aeval, CliffordAlgebra.map_surjective, Polynomial.Splits.image_rootSet_of_map_ne_zero, Polynomial.contDiff_aeval, IsAdjoinRoot.ofAlgEquiv_map_apply, derivationToSquareZeroEquivLift_apply_coe_apply, FiniteGaloisIntermediateField.adjoin_simple_map_algHom, ExteriorAlgebra.lift_unique, WeierstrassCurve.Affine.baseChange_slope, BoundedContinuousFunction.toContinuousMapâ_apply, Algebra.Generators.aeval_val_Ï', Polynomial.mem_rootSet, AdjoinRoot.aeval_algHom_eq_zero, Algebra.Generators.Hom.comp_val, AlgCat.forgetâ_module_map, Polynomial.map_under_lt_comap_of_quasiFiniteAt, trace_eq_sum_embeddings, AlgHom.prodEquiv_apply, MvPolynomial.comap_apply, IsAdjoinRoot.map_eq_zero_iff, MulSemiringAction.toAlgHom_apply, MvPolynomial.vars_rename, CommRingCat.Under.equalizerFork_Îč, WittVector.bindâ_zero_wittPolynomial, Algebra.FormallySmooth.exists_adicCompletionEvalOneâ_comp_eq, Polynomial.exists_separable_of_irreducible, MvPowerSeries.coeff_killCompl, Polynomial.roots_expand_image_iterateFrobenius, IntermediateField.val_mk, DoubleQuot.quotQuotEquivQuotOfLEâ_toRingEquiv, MatrixEquivTensor.right_inv, Algebra.FormallyUnramified.iff_comp_injective, CommAlgCat.reflectsIsomorphisms_forget, AdicCompletion.evalâ_of, Module.End.lTensorAlgHom_apply_apply, PowerSeries.expand_monomial, Polynomial.aeval_monomial, MvPowerSeries.aeval_eq_sum, Polynomial.eval_map_algebraMap, Unitization.lift_range_le, AlgHom.normal_bijective, StandardEtalePresentation.toPresentation_val, Polynomial.algEquivOfCompEqX_apply, Polynomial.mem_rootSet_of_ne, Polynomial.mapAlg_comp, TrivSqZeroExt.lift_apply_inl, AlgHom.down_ulift_apply, IsAdjoinRoot.aeval_root_self, RingHom.toIntAlgHom_coe, Polynomial.aeval_eq_sum_range', MvPolynomial.rename_comp_bindâ, Polynomial.expand_char, Polynomial.aeval_zero, IntermediateField.nonempty_algHom_of_adjoin_splits, MvPolynomial.rename_X, pinGroup.involute_act_Îč_mem_range_Îč, LinearAlgebra.FreeProduct.lift_algebraMap, SymmetricAlgebra.algebraMap_leftInverse, ContinuousAlgHom.coe_coe, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, conductor_mul_differentIdeal, IntermediateField.inclusion_inclusion, Module.AEval.annihilator_top_eq_ker_aeval, CliffordAlgebra.EquivEven.involute_e0, RatFunc.liftAlgHom_apply_div', Polynomial.roots_expand_pow_image_iterateFrobenius_subset, AlgEquiv.ofAlgHom_apply, FiniteField.nonempty_algHom_iff_finrank_dvd, MvPolynomial.aeval_one_tmul, minpoly.eq_iff_aeval_minpoly_eq_zero, Algebra.discr_powerBasis_eq_prod'', Polynomial.algEquivCMulXAddC_symm_apply, TensorAlgebra.algebraMap_leftInverse, MvPowerSeries.IsNilpotent_subst, WeierstrassCurve.Affine.baseChange_addY, PowerSeries.coeff_expand, Polynomial.algEquivOfTranscendental_symm_aeval, AdicCompletion.evalOneâ_surjective, AlgHom.mk_coe, CliffordAlgebra.evenEquivEvenNeg_symm_apply, Polynomial.algHom_evalâ_algebraMap, Polynomial.IsMonicOfDegree.aeval_sub, AdicCompletion.factor_evalâ_eq_eval, MvPolynomial.finSuccEquiv_rename_finSuccEquiv, TrivSqZeroExt.map_inl, PowerSeries.coe_aeval, MvPolynomial.rename_expand, CliffordAlgebraComplex.toComplex_involute, ContinuousMap.polynomial_comp_attachBound, Polynomial.expand_eval, WeierstrassCurve.Projective.baseChange_neg, PowerBasis.equivOfRoot_aeval, AdicCompletion.evalâ_comp_liftRingHom, isAlgebraic_iff_not_injective, LinearAlgebra.FreeProduct.lift_symm_apply, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, CliffordAlgebraComplex.toComplex_ofComplex, MvPolynomial.aeval_sumElim_pderiv_inl, FiniteField.expand_card, AnalyticAt.aeval_mvPolynomial, AlgHom.map_algebraMap, RingQuot.preLiftAlgHom_def, Polynomial.coeff_expand_mul', Polynomial.differentiableWithinAt_aeval, Unitization.norm_splitMul_snd_sq, AdjoinRoot.coe_algEquivOfEq, IntermediateField.exists_algHom_of_splits_of_aeval, ContinuousMap.evalAlgHom_apply, WeakDual.CharacterSpace.equivAlgHom_coe, AlgCat.forgetâRing_preservesLimits, AdjoinRoot.aeval_eq, CliffordAlgebra.lift_comp_Îč, Algebra.subsingleton_id, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, MvPowerSeries.comp_subst, AlgEquiv.arrowCongr_symm, Polynomial.coeff_zero_eq_aeval_zero', Ideal.Quotient.liftâ_apply, MvPolynomial.isSymmetric_rename, CliffordAlgebra.ofEven_Îč, AdjoinRoot.liftHom_of, AlgEquiv.toLinearMap_ofBijective, CliffordAlgebra.ofBaseChange_tmul_one, Polynomial.roots_expand_pow, MvPolynomial.universalFactorizationMap_freeMonic, AlgHom.map_adjoin_singleton, Subalgebra.toSubring_subtype, AdjoinRoot.equiv'_apply, AnalyticOnNhd.aeval_polynomial, Algebra.Generators.Hom.toAlgHom_monomial, IntermediateField.nonempty_algHom_of_splits, DualNumber.lift_apply_inl, MvPolynomial.coe_expand, Polynomial.contract_mul_expand, Polynomial.algEquivAevalXAddC_apply, MvPolynomial.aeval_sumElim, Polynomial.map_frobenius_expand, Algebra.TensorProduct.liftEquiv_symm_apply_coe, Unitization.splitMul_injective, AddMonoidAlgebra.decomposeAux_single, MulSemiringAction.toAlgHom_injective, DualNumber.lift_op_smul, MvPolynomial.support_rename_killCompl_subset, AlgHom.toEnd_apply, MvPolynomial.evalâ_rename_prod_mk, Polynomial.mapAlgHom_eq_evalâAlgHom_CAlgHom, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, CliffordAlgebra.toBaseChange_Îč, Polynomial.newtonMap_apply, Derivation.apply_aeval_eq', Subalgebra.LinearDisjoint.linearIndependent_left_of_flat, AdicCompletion.evalâ_mk, WeierstrassCurve.Affine.Equation.baseChange, Representation.asModuleEquiv_map_smul, Algebra.discr_powerBasis_eq_prod', MvPolynomial.mapAlgHom_coe_ringHom, Subalgebra.iSupLift_inclusion, DoubleQuot.quotQuotEquivComm_comp_quotQuotMkâ, Polynomial.aevalTower_comp_C, Subalgebra.centralizer_coe_image_includeLeft_eq_center_tensorProduct, bindâ_wittPolynomial_xInTermsOfW, PowerSeries.coe_rescaleAlgHom, Ideal.KerLift.map_smul, Polynomial.coe_aeval_eq_eval, Algebra.FinitePresentation.out, Matrix.aeval_self_charpoly, AlgHom.toRingHom_toAddMonoidHom, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, ContinuousMap.compRightAlgHom_continuous, MvPolynomial.rename_leftInverse, LinearAlgebra.FreeProduct.lift_apply, PowerBasis.liftEquiv'_symm_apply_apply, AlgHom.IsArithFrobAt.restrict_mk, AdicCompletion.evalâ_mkâ, Algebra.FiniteType.iff_quotient_mvPolynomial'', Algebra.TensorProduct.includeRight_surjective, MvPolynomial.esymmAlgHom_fin_bijective, RingHom.toNatAlgHom_apply, IntermediateField.AdjoinSimple.coe_aeval_gen_apply, AlgHom.coe_codRestrict, IsLocalization.Away.mapâ_apply, MvPolynomial.esymmAlgEquiv_apply, MvPolynomial.evalâAlgHom_X, PowerSeries.aeval_coe, card_algHom_le_finrank, MvPolynomial.mem_vanishingIdeal_iff, MvPolynomial.mem_vanishingIdeal_singleton_iff, gelfandTransform_isometry, Quaternion.coe_ofComplex, MonoidAlgebra.singleOneAlgHom_apply, Submodule.coe_mapAlgHom_apply, AlgHom.toKerIsLocalization_isLocalizedModule, MonoidAlgebra.lift_def, MvPolynomial.expand_zmod, PowerSeries.coeff_heval_zero, CliffordAlgebra.involute_involutive, minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C, Subalgebra.val_mulMap'_tmul, IsAdjoinRoot.liftHom_algEquiv, Polynomial.Monic.expand, MvPolynomial.aeval_zero', MvPolynomial.weightedTotalDegree_rename_of_injective, Polynomial.aeval_iterate_derivative_of_lt, Ideal.comap_fiberIsoOfBijectiveResidueField_symm, WeierstrassCurve.Projective.baseChange_polynomialZ, PowerSeries.substAlgHom_coe, DualNumber.lift_comp_inlHom, AlgHom.linearMapMk_toAddHom, MvPowerSeries.coeff_rename_eq_zero, Field.nonempty_algHom_of_minpoly_eq, AddMonoidAlgebra.decomposeAux_eq_decompose, MvPolynomial.rename_toMvPolynomial, Polynomial.natDegree_expand, MvPolynomial.aeval_rename, LieRinehartAlgebra.Hom.apply_lie', Module.Basis.traceDual_powerBasis_eq, WittVector.bindâ_frobeniusPolyRat_wittPolynomial, CommBialgCat.forgetâ_commAlgCat_map, WeakDual.CharacterSpace.equivAlgHom_symm_coe, Polynomial.aeval_pi_applyâ, Unitization.lift_apply_apply, WittVector.aeval_verschiebungPoly, Ideal.map_idâ, MvPolynomial.evalâHom_bindâ, MvPowerSeries.coeff_rename, Algebra.TensorProduct.tensorQuotientEquiv_apply_tmul, MvPolynomial.degreeOf_eq_natDegree, cardinalMk_algHom, MvPowerSeries.support_expand_subset, CliffordAlgebra.involuteEquiv_symm_apply, Polynomial.aeval_mem_adjoin_singleton, PowerSeries.expand_X, Algebra.coe_lmul_eq_mul, ExteriorAlgebra.comp_Îč_sq_zero, DoubleQuot.coe_quotQuotEquivCommâ, Polynomial.toAddCircle_X_eq_fourier_one, MvPolynomial.bindâ_X_right, MvPolynomial.coeff_rename_eq_zero, CliffordAlgebra.ofProd_Îč_mk, CliffordAlgebra.GradedAlgebra.lift_Îč_eq, Polynomial.tendsto_abv_aeval_atTop, AddMonoidAlgebra.lift_unique, MvPolynomial.evalâHom_C_left, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, MvPolynomial.aeval_monomial, Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly, AddMonoidAlgebra.lift_def, Polynomial.cyclotomic_expand_eq_cyclotomic, Algebra.trace_apply, Polynomial.toMvPolynomial_injective, TensorAlgebra.toDirectSum_Îč, AddMonoidAlgebra.singleZeroAlgHom_apply, ExteriorAlgebra.leftInverse_map_iff, Field.nonempty_algHom_of_aeval_eq_zero_subset, AlgHom.toRingHom_toMonoidHom, AlgEquiv.toAlgHomHom_apply, Complex.ofRealAm_coe, WeierstrassCurve.Affine.baseChange_polynomialY, Algebra.FormallySmooth.exists_kerProj_comp_eq_id, Algebra.smulTower_leftMulMatrix_algebraMap_eq, lipschitzGroup.involute_act_Îč_mem_range_Îč, AlgHom.injective_codRestrict, WeierstrassCurve.Affine.baseChange_addX, Polynomial.aeval_algHom_apply, Polynomial.coe_toLaurentAlg, AlgEquiv.arrowCongr_refl, WittVector.mul_polyOfInterest_aux3, TensorAlgebra.lift_unique, AddMonoidAlgebra.scalarTensorEquiv_tmul, Polynomial.shiftedLegendre_eval_symm, Polynomial.aevalAevalEquiv_apply, Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits, MvPolynomial.aeval_prod, RatFunc.algEquivOfTranscendental_algebraMap, IsPurelyInseparable.instNonemptyAlgHomOfPerfectField, RatFunc.aeval_X_left_eq_algebraMap, IsLocalization.algHom_subsingleton, Matrix.toMvPolynomial_mul, LinearAlgebra.FreeProduct.lift_comp_Îč, Subalgebra.toSubsemiring_subtype, minpoly.aeval_of_isScalarTower, MvPolynomial.exists_restrict_to_vars, wittStructureInt_rename, TensorProduct.AlgebraTensorModule.range_lTensor_idealMap, AlgHom.restrictNormal_commutes, FiniteField.orderOf_frobeniusAlgHom, MvPowerSeries.killCompl_X, TrivSqZeroExt.fstHom_apply, Polynomial.mapAlgHom_coe_ringHom, AlgHom.subsingleton, AdjoinRoot.liftHom_root, MvPowerSeries.rename_X, MvPolynomial.aevalTower_algebraMap, TrivSqZeroExt.liftEquiv_symm_apply_coe, Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor, Polynomial.expand_aeval, PowerSeries.substAlgHom_comp_substAlgHom_apply, AlgHom.id_toRingHom, Field.finSepDegree_eq_of_adjoin_splits, AlgHom.toOpposite_apply, Subalgebra.mulMap_tmul, RingCon.liftâ_mk, WeierstrassCurve.Jacobian.baseChange_negY, BialgCat.forgetâ_algebra_obj, PowerBasis.lift_gen, Polynomial.aeval_natCast, MvPowerSeries.killCompl_C, AlgHom.kerSquareLift_mk, trace_eq_sum_embeddings_gen, MvPolynomial.eval_expand, AlgHom.card_of_splits, algebraMap_galRestrict'_apply, Polynomial.aeval_algHom, Polynomial.coe_aevalAeval_eq_evalEval, Polynomial.IsSplittingField.IsScalarTower.splits, PowerBasis.aeval_minpolyGen, Polynomial.coe_aeval_eq_evalRingHom, AdjoinRoot.coe_algHomOfDvd, galRestrictHom_apply, RingCon.coe_liftâ, Polynomial.toLaurentAlg_apply, MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subset, IsSymmetricAlgebra.equiv_toAlgHom, FiniteField.coe_frobeniusAlgHom, MvPolynomial.evalâAlgHom_apply, Algebra.IsAlgebraic.bijective_of_isScalarTower, WeierstrassCurve.Projective.baseChange_dblY, MonoidAlgebra.mapDomainAlgHom_apply, Pi.evalAlgHom_apply, AdjoinRoot.liftAlgHom_root, TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_Îč_eq_Îč, AlgebraicGeometry.pullbackSpecIso_hom_snd, IntermediateField.mem_map, MvPolynomial.killCompl_monomial, IntermediateField.normalClosure_def', Algebra.TensorProduct.map_bijective, Subalgebra.map_toSubsemiring, spectrum.map_polynomial_aeval, IsAlgClosed.surjective_restrictDomain_of_isAlgebraic, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, spinGroup.involute_eq, DoubleQuot.quotLeftToQuotSupâ_toRingHom, Ideal.ResidueField.liftâ_algebraMap, Algebra.Extension.Cotangent.map_mk, MatrixEquivTensor.toFunAlgHom_apply, Polynomial.aevalAeval_C, PowerSeries.heval_mul, Polynomial.toAddCircle_C_eq_smul_fourier_zero, PowerBasis.constr_pow_aeval, Quaternion.hom_ext_iff, Polynomial.algHom_ext'_iff, Polynomial.isLocalHom_expand, Algebra.norm_eq_prod_embeddings_gen, AlgEquiv.toAlgHom_apply, MvPolynomial.rename_hsymm, RCLike.ofRealAm_coe, CommAlgCat.id_apply, SkewMonoidAlgebra.lift_def, AlgCat.ofHom_apply, Ideal.quotient_map_mkâ, MvPolynomial.aeval_natDegree_le, IsAdjoinRoot.lift_algebraMap_apply, Derivation.compAEval_apply, C_p_pow_dvd_bindâ_rename_wittPolynomial_sub_sum, matPolyEquiv_eq_X_pow_sub_C, Algebra.leftMulMatrix_eq_repr_mul, Algebra.Generators.Hom.algebraMap_toAlgHom, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, AdjoinRoot.liftHom_mk, AlgHom.op_symm_apply_apply, Polynomial.Bivariate.Transcendental.algEquivAdjoin_swap_eq_aeval, AlgHom.toLieHom_apply, DoubleQuot.quotQuotEquivQuotSupâ_symm_toRingEquiv, WittVector.coeff_frobenius, Matrix.aeval_eq_aeval_mod_charpoly, RingCon.quotientQuotientEquivQuotientâ_coe_coe, AlgEquiv.ofBijective_apply_symm_apply, Polynomial.aeval_algebraMap_apply, Algebra.Generators.comp_Ï, CliffordAlgebraQuaternion.toQuaternion_Îč, Unitization.lift_apply, WeierstrassCurve.Projective.baseChange_addY, Polynomial.fourierCoeff_toAddCircle, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, Module.AEval.mem_mapSubmodule_apply, CommAlgCat.forgetâ_commRingCat_map, algebraMap_galRestrictHom_apply, Algebra.prod_embeddings_eq_finrank_pow, CliffordAlgebra.reverseOpEquiv_apply, Representation.asAlgebraHom_mem_of_forall_mem, MvPowerSeries.subst_coe, AddMonoidAlgebra.isLocalHom_singleZeroAlgHom, FiniteField.card_algHom_of_finrank_dvd, MvPolynomial.mapEquivMonic_symm_map_algebraMap, MvPolynomial.coe_aeval_eq_eval, FreeAlgebra.hom_ext_iff, AlgHom.ulift_apply, BialgCat.MonoidalCategory.inducingFunctorData_ΔIso, FreeAlgebra.algebraMap_leftInverse, IsSepClosed.surjective_restrictDomain_of_isSeparable, RingHom.toIntAlgHom_injective, exists_integral_inj_algHom_of_fg, Algebra.FormallyUnramified.iff_exists_tensorProduct, Ideal.Quotient.mkâ_surjective, RingCon.liftâ_coe_toRingHom, Polynomial.map_aeval_eq_aeval_map, WeierstrassCurve.Jacobian.baseChange_addY, AlgHom.toFun_eq_coe, MvPowerSeries.substAlgHom_apply, AlgHom.prod_apply, WeierstrassCurve.Affine.baseChange_negAddY, ContinuousMap.compRightAlgHom_apply, AdjoinRoot.algHomOfDvd_apply_root, Module.AEval.annihilator_eq_ker_aeval, DividedPowerAlgebra.mkAlgHom_C, Ideal.map_includeLeft_eq, Polynomial.aeval_add, Polynomial.continuousOn_aeval, CliffordAlgebra.equivOfIsometry_apply, MvPowerSeries.substAlgHom_comp_substAlgHom, Polynomial.aeval_sub, Algebra.TensorProduct.rTensor_ker, WeierstrassCurve.baseChange_Κâ, IsAdjoinRoot.map_surjective, Polynomial.continuousAt_aeval, IsSepClosed.exists_aeval_eq_zero, Module.End.eigenspace_aeval_polynomial_degree_1, inv_eq_of_aeval_divX_ne_zero, instSubsingletonAlgHomOfIsPurelyInseparable, Polynomial.exists_monic_aeval_eq_zero_forall_mem_of_mem_map, RatFunc.algEquivOfTranscendental_apply, CliffordAlgebra.map_mul_map_eq_neg_of_isOrtho_of_mem_evenOdd_one, LieAlgebra.ExtendScalars.map_apply_tmul, MvPowerSeries.HasSubst.expand, Algebra.TensorProduct.mapOfCompatibleSMul_tmul, Algebra.leftMulMatrix_apply, PowerSeries.coe_substAlgHom, Ideal.ResidueField.mapâ_apply, Transcendental.aeval_of_transcendental, MvPolynomial.hom_bindâ, MvPolynomial.coeff_expand_zero, DoubleQuot.coe_liftSupQuotQuotMkâ, Polynomial.aeval_X, CommRingCat.coproductCocone_Îč, AdicCompletion.evalOneâ_liftAlgHom, Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, CliffordAlgebra.leftInverse_map_of_leftInverse, AdjoinRoot.mkâ_toRingHom, Matrix.mvPolynomialX_mapMatrix_aeval, IsAdjoinRoot.algEquiv_apply_map, AlgHom.range_toSubsemiring, Polynomial.roots_expand_map_frobenius_le, AlgebraicGeometry.Proj.lift_awayMapâ_awayMapâ_surjective, AdicCompletion.evalâ_liftRingHom, AlgHom.coe_toAddMonoidHom, CliffordAlgebra.EquivEven.involute_v, Polynomial.aeval_homogenize_of_eq_one, MonoidAlgebra.lift_single, GradedAlgHom.coe_mk, Polynomial.toContinuousMapOnAlgHom_apply, Algebra.FormallyEtale.comp_bijective, IsAdjoinRoot.ker_map, Polynomial.coe_mapAlgHom, Algebra.Extension.Hom.toAlgHom_apply, MvPolynomial.rename_eq, IsSymmetricAlgebra.lift_comp_linearMap, AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure, RingHom.equivRatAlgHom_symm_apply, WeierstrassCurve.Jacobian.baseChange_negAddY, IntermediateField.coe_map, MvPolynomial.mapEquivMonic_symm_map, MonoidAlgebra.toRingHom_mapAlgHom, Algebra.FormallySmooth.iff_comp_surjective, IntermediateField.Lifts.nonempty_algHom_of_exist_lifts_finset, AlgEquiv.algHomUnitsEquiv_apply_apply, Algebra.SubmersivePresentation.basisDeriv_apply, MvPolynomial.bindâ_monomial, RingCon.coe_quotientKerEquivRangeâ_mkâ, LocallyConstant.toContinuousMapAlgHom_apply, Ideal.kerLiftAlg_mk, AlgHom.End_toSemigroup_toMul_mul, UniversalEnvelopingAlgebra.lift_Îč_apply', Algebra.TensorProduct.linearEquivIncludeRange_tmul, RingQuot.eq_liftAlgHom_comp_mkAlgHom, MvPolynomial.coeff_killCompl, Algebra.lsmul_coe, AlgHom.IsArithFrobAt.restrict_apply, Algebra.TensorProduct.includeLeft_surjective, IsAlgClosed.exists_aeval_eq_zero, LieRinehartAlgebra.Hom.apply_lie, Polynomial.expand_injective, MvPolynomial.esymmAlgHom_surjective, MvPolynomial.aevalTower_ofNat, MvPolynomial.killCompl_monomial_eq_zero_of_notMem_range, CommRingCat.Under.equalizer_comp, AlgHom.coe_pow, inv_eq_of_root_of_coeff_zero_ne_zero, IsScalarTower.toAlgHom_apply, Polynomial.aevalAevalEquiv_symm_apply_fst, Polynomial.map_iterateFrobenius_expand, retractionOfSectionOfKerSqZero_tmul_D, MvPolynomial.rename_surjective, AlgCat.instIsRightAdjointForgetAlgHomCarrier, Polynomial.evalâ_algebraMap_X, FractionalIdeal.map_mem_map, CommRingCat.Under.equalizerFork'_Îč, MvPolynomial.evalâHom_comp_expand, LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul, MvPowerSeries.expand_C, Polynomial.toMvPolynomial_C, Subalgebra.coe_inclusion, AdjoinRoot.coe_ofAlgHom, WeierstrassCurve.VariableChange.map_baseChange, AlgHom.coe_monoidHom_injective, RingQuot.mkAlgHom_coe, Polynomial.aevalAevalEquiv_symm_apply, Algebra.Generators.Hom.equivAlgHom_apply_coe, MonoidAlgebra.lift_of, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, cfc_comp_polynomial, IntermediateField.nonempty_algHom_adjoin_of_splits, MvPolynomial.esymmAlgHom_injective, MvPolynomial.expand_zero_apply, Polynomial.expand_pow, PowerBasis.liftEquiv_apply_coe, IsFractionRing.liftAlgHom_apply, IsAzumaya.AlgHom.mulLeftRight_bij, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', IntermediateField.LinearDisjoint.linearIndependent_left, MvPolynomial.renameSymmetricSubalgebra_apply_coe, Algebra.FinitePresentation.iff_quotient_mvPolynomial', IsAdjoinRootMonic.modByMonic_repr_map, Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero, AlgEquiv.coe_ringHom_commutes, MvPolynomial.coe_mapEquivMonic_comp, MvPolynomial.transcendental_supported_polynomial_aeval_X, Algebra.FormallyUnramified.iff_comp_injective_of_small, Polynomial.aeval_sumIDeriv_of_pos, Polynomial.continuousWithinAt_aeval, CliffordAlgebraQuaternion.ofQuaternion_toQuaternion, MvPolynomial.pderiv_inl_universalFactorizationMap_X, SkewMonoidAlgebra.lift_symm_apply, AlgHom.id_apply, MonoidAlgebra.lift_unique', KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span, Algebra.TensorProduct.closure_range_union_range_eq_top, AdjoinRoot.coe_algEquivOfAssociated, Derivation.apply_aeval_eq, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, LocallyConstant.comapâ_apply_apply, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply, AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc, MvPolynomial.rTensorAlgHom_apply_eq
|