Hom

📁 Source: Mathlib/Algebra/Algebra/Hom.lean

Statistics

Metric	Count
Definitions AlgHom, apply, coeOutAddMonoidHom, coeOutMonoidHom, comp, funLike, id, mk', ofLinearMap, toAddMonoidHom', toEnd, toLinearMap, toMonoidHom', toRingHom, AlgHomClass, coeTC, toAlgHom, algHom, instMulDistribMulActionAlgHomUnits, ofId, toAlgHom, toIntAlgHom, toNatAlgHom, uniqueOfRight, «term_→ₐ[_]_», «term_→ₐ_»	26
Theorems End_toOne_one, End_toSemigroup_toMul_mul, addHomMk_coe, algHomClass, algebraMap_eq_apply, cancel_left, cancel_right, coe_addMonoidHom_injective, coe_coe, coe_comp, coe_fn_inj, coe_fn_injective, coe_id, coe_mk, coe_mk', coe_mks, coe_monoidHom_injective, coe_pow, coe_ringHom_injective, coe_ringHom_mk, coe_toAddMonoidHom, coe_toLinearMap, coe_toMonoidHom, coe_toRingHom, commutes, commutes', comp_algebraMap, comp_apply, comp_assoc, comp_id, comp_toLinearMap, comp_toRingHom, congr_arg, congr_fun, default_apply, ext, ext_iff, id_apply, id_comp, id_toRingHom, instRingHomCompTripleComp, linearMapMk_toAddHom, map_smul_of_tower, mk_coe, mul_apply, ofLinearMap_apply, ofLinearMap_id, ofLinearMap_toLinearMap, one_apply, toEnd_apply, toFun_eq_coe, toLinearMap_apply, toLinearMap_id, toLinearMap_injective, toLinearMap_ofLinearMap, toRingHom_eq_coe, toRingHom_toAddMonoidHom, toRingHom_toMonoidHom, commutes, linearMapClass, toLinearMap_toAlgHom, toRingHomClass, toRingHom_toAlgHom, algebraMapSubmonoid_le_comap, algebraMapSubmonoid_map_eq, comp_ofId, ext_id, ext_id_iff, ofId_apply, ofId_self, smul_units_def, subsingleton_id, toRingHom_ofId, toAlgHom_apply, toAlgHom_injective, toIntAlgHom_apply, toIntAlgHom_coe, toIntAlgHom_injective, toNatAlgHom_apply, toNatAlgHom_coe	80
Total	106

AlgHom

Definitions

Name	Category	Theorems
coeOutAddMonoidHom 📖	CompOp	—
coeOutMonoidHom 📖	CompOp	—
comp 📖	CompOp	230 math math: Subalgebra.mulMap_comm, IntermediateField.exists_algHom_adjoin_of_splits, Algebra.TensorProduct.lift_comp_includeLeft, comp_toRingHom, Ideal.comap_comapₐ, MvPolynomial.universalFactorizationMap_comp_map, val_comp_codRestrict, comp_toLinearMap, Ideal.Quotient.factorₐ_comp_mk, ExteriorAlgebra.map_comp_map, MvPolynomial.algHom_ext'_iff, Algebra.TensorProduct.map_comp, IntermediateField.algHomEquivAlgHomOfSplits_apply, Bialgebra.TensorProduct.counitAlgHom_def, Pi.algHom_comp, snd_prod, ExteriorAlgebra.toTrivSqZeroExt_comp_map, CliffordAlgebra.toProd_comp_ofProd, IntermediateField.exists_algHom_of_adjoin_splits, MvPolynomial.killCompl_comp_rename, TrivSqZeroExt.fstHom_comp_map, CommRingCat.toAlgHom_comp, CliffordAlgebraComplex.toComplex_comp_ofComplex, RingCon.quotientKerEquivRangeₐ_comp_mkₐ, Polynomial.mapAlgHom_eq_eval₂AlgHom'_CAlgHom, RingCon.coe_comapQuotientEquivRangeₐ_mk, MvPolynomial.comap_comp_apply, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd, RingCon.mkₐ_comp_factorₐ_comp_mkₐ, Subalgebra.mulMap_map_comp_eq, comp_assoc, AdjoinRoot.algHom_ext'_iff, val_comp_rangeRestrict, RingQuot.ringQuot_ext'_iff, AlgebraicIndependent.aeval_comp_repr, Algebra.comp_ofId, Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap, AlgEquiv.arrowCongr_apply, range_comp_le_range, Polynomial.Monic.quotient_isIntegral, MvPolynomial.sumAlgEquiv_comp_rename_inr, CliffordAlgebra.toBaseChange_comp_ofBaseChange, MvPowerSeries.comp_aeval, Normal.algHomEquivAut_symm_apply, Localization.algHom_ext_iff, IntermediateField.map_map, Field.Emb.Cardinal.succEquiv_coherence, TrivSqZeroExt.algHom_ext'_iff, toAlgHom_comp_sectionOfRetractionKerToTensorAux, CliffordAlgebra.toBaseChange_comp_involute, MvPolynomial.expand_zero, Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap, MvPolynomial.coe_mapEquivMonic_comp', toUnder_comp, Polynomial.toMvPolynomial_eq_rename_comp, TrivSqZeroExt.map_comp_inlAlgHom, id_comp, AlgCat.ofHom_comp, IntermediateField.fieldRange_comp_val, MvPolynomial.comap_comp, comp_apply, Bialgebra.TensorProduct.comulAlgHom_def, Algebra.FormallySmooth.comp_lift, prodEquiv_symm_apply, Algebra.TensorProduct.productMap_left, Subalgebra.mulMap_bot_left_eq, KaehlerDifferential.End_equiv_aux, MvPolynomial.rename_comp_expand, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst, PowerSeries.substAlgHom_comp_substAlgHom, comap_ker, MvPolynomial.bind₁_comp_bind₁, MonoidAlgebra.mapDomainAlgHom_comp, Algebra.FormallySmooth.exists_mkₐ_comp_eq_of_isAdicComplete, galLift_comp, FiniteType.comp_surjective, Ideal.ResidueField.liftₐ_comp_toAlgHom, RingQuot.liftAlgHom_def, CliffordAlgebra.involute_comp_involute, IsAzumaya.mulLeftRight_comp_congr, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, FractionalIdeal.map_comp, CommAlgCat.hom_comp, cancel_right, Algebra.lift_algHom_comp_left, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ, Algebra.TensorProduct.lmul'_comp_map, MvPowerSeries.rescaleAlgHom_mul, MvPolynomial.sumAlgEquiv_comp_rename_inl, Algebra.TensorProduct.lift_comp_includeRight, CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion, MvPolynomial.rename_esymmAlgHom, map_fieldRange, IntermediateField.exists_algHom_of_splits, IntermediateField.Lifts.lt_iff, mapMatrix_comp, GradedTensorProduct.algHom_ext_iff, CliffordAlgebra.toEven_comp_ofEven, BialgHomClass.counitAlgHom_comp, AlgEquiv.symm_comp, Algebra.TensorProduct.productMap_eq_comp_map, Algebra.FormallyUnramified.comp_injective, Algebra.TensorProduct.lmul'_comp_includeRight, WeakDual.CharacterSpace.compContinuousMap_apply, Algebra.TensorProduct.map_comp_id, AdjoinRoot.mapAlgHom_comp_mapAlghom, derivationToSquareZeroEquivLift_symm_apply_apply_coe, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ, AlgEquiv.arrowCongr_comp, Algebra.FormallySmooth.exists_lift, Algebra.TensorProduct.comm_comp_includeRight, Algebra.TensorProduct.comm_comp_includeLeft, MvPolynomial.comp_aeval, RingCon.coe_comapQuotientEquivRangeₐ_symm_mk, Algebra.FormallySmooth.comp_surjective, Subalgebra.mulMap_bot_right_eq, Algebra.FormallyEtale.iff_comp_bijective, PiTensorProduct.algHom_ext_iff, MvPowerSeries.expand_comp_substAlgHom, DualNumber.coe_lift_symm_apply, coe_comp, WeierstrassCurve.Affine.Point.map_map, CliffordAlgebra.toBaseChange_comp_reverseOp, MvPolynomial.rename_comp_toMvPolynomial, TensorAlgebra.toDirectSum_comp_ofDirectSum, AlgebraicIndependent.liftAlgHom_comp_reprField, Algebra.TensorProduct.map_range, RingCon.comapQuotientEquivRangeₐ_mk, Algebra.TensorProduct.map_comp_includeRight, MvPolynomial.bind₁_comp_rename, TrivSqZeroExt.map_comp_map, PowerSeries.expand_mul_eq_comp, Algebra.FormallySmooth.iff_split_surjection, CliffordAlgebra.ofEven_comp_toEven, Algebra.TensorProduct.ext_iff, Ideal.ResidueField.algHom_ext_iff, AddMonoidAlgebra.mapDomainAlgHom_comp, FiniteType.comp, PowerSeries.comp_aeval, Algebra.FormallySmooth.comp_liftOfSurjective, MvPolynomial.expand_comp_bind₁, MvPolynomial.aeval_comp_bind₁, cancel_left, DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ, Algebra.lift_algHom_comp_right, toAlgHom_comp_sectionOfRetractionKerToTensor, Finite.comp, BialgHomClass.map_comp_comulAlgHom, StandardEtalePresentation.toPresentation_σ', CliffordAlgebra.ofProd_comp_toProd, MvPolynomial.aeval_comp_expand, Ideal.map_mapₐ, MvPolynomial.aevalTower_comp_toAlgHom, Ideal.quotient_map_comp_mkₐ, Subalgebra.range_comp_val, TrivSqZeroExt.lift_comp_inlHom, restrictNormal_comp, toLieHom_comp, FinitePresentation.comp, AlgEquiv.comp_symm, Algebra.TensorProduct.lift_comp_includeRight', liftOfSurjective_comp, Polynomial.aeval_algEquiv, derivationToSquareZeroEquivLift_apply_coe_apply, ContinuousAlgEquiv.comp_coe, Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq, Algebra.TensorProduct.lmul'_comp_includeLeft, Algebra.FormallyUnramified.iff_comp_injective, MvPolynomial.rename_comp_bind₁, ContinuousAlgHom.coe_comp, CliffordAlgebraQuaternion.ofQuaternion_comp_toQuaternion, comp_id, Algebra.TensorProduct.comm_comp_map, LinearAlgebra.FreeProduct.lift_symm_apply, MvPolynomial.rename_comp_rename, Algebra.TensorProduct.map_restrictScalars_comp_includeRight, MvPolynomial.aeval_comp_rename, Algebra.TensorProduct.liftEquiv_symm_apply_coe, FinitePresentation.comp_surjective, Subalgebra.val_comp_inclusion, fst_prod, DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ, IsAdjoinRoot.algEquiv_map, Polynomial.mapAlgHom_comp, AlgCat.hom_comp, instRingHomCompTripleComp, Ideal.Quotient.factorₐ_comp, DualNumber.lift_comp_inlHom, DualNumber.algHom_ext'_iff, CliffordAlgebraComplex.ofComplex_comp_toComplex, Algebra.TensorProduct.lmul''_eq_lid_comp_mapOfCompatibleSMul, Algebra.TensorProduct.productMap_right, StandardEtalePresentation.toPresentation_relation, galRestrict'_comp, Algebra.FormallySmooth.exists_kerProj_comp_eq_id, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, LinearAlgebra.FreeProduct.lift_comp_ι, BialgHom.comp_toAlgHom, IntermediateField.Lifts.eq_iff, TrivSqZeroExt.liftEquiv_symm_apply_coe, TensorAlgebra.ofDirectSum_comp_toDirectSum, Polynomial.aevalTower_comp_toAlgHom, Algebra.TensorProduct.map_id_comp, MvPolynomial.aeval_comp_toMvPolynomial, Polynomial.aeval_algHom, MvPolynomial.expand_mul_eq_comp, MvPowerSeries.expand_mul_eq_comp, MvPowerSeries.comp_substAlgHom, Polynomial.algHom_ext'_iff, CliffordAlgebra.evenToNeg_comp_evenToNeg, CommAlgCat.ofHom_comp, prod_comp, range_comp, MvPolynomial.mapEquivMonic_symm_map_algebraMap, Ideal.Quotient.liftₐ_comp, CliffordAlgebra.ofBaseChange_comp_toBaseChange, MvPowerSeries.substAlgHom_comp_substAlgHom, CliffordAlgebra.map_comp_map, Algebra.TensorProduct.map_comp_includeLeft, Subalgebra.map_map, IntermediateField.Lifts.le_iff, Algebra.FormallyEtale.comp_bijective, MvPolynomial.mapEquivMonic_symm_map, Algebra.FormallySmooth.iff_comp_surjective, End_toSemigroup_toMul_mul, RingQuot.eq_liftAlgHom_comp_mkAlgHom, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', MvPolynomial.coe_mapEquivMonic_comp, Algebra.FormallyUnramified.iff_comp_injective_of_small
funLike 📖	CompOp	1624 math math: CommRingCat.tensorProd_map_right, CliffordAlgebra.unop_reverseOp, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, MvPolynomial.join₁_rename, IsSymmetricAlgebra.lift_eq, 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, coe_toLinearMap, RatFunc.laurent_injective, TensorAlgebra.ofDirectSum_of_tprod, mem_range_self, Bialgebra.comulAlgHom_apply, Subalgebra.inclusion_right, PowerSeries.hasSum_aeval, Polynomial.rootSet_mapsTo, minpoly.ToAdjoin.injective, Polynomial.mem_aroots', CommAlgCat.comp_apply, SymmetricAlgebra.lift_ι_apply, AddMonoidAlgebra.lift_apply', MvPolynomial.algHom_ext_iff, MvPolynomial.map_bind₁, CliffordAlgebra.involute_eq_of_mem_odd, Algebra.Generators.aeval_val_surjective, 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, Polynomial.roots_expand, Pi.constAlgHom_apply, Polynomial.algEquivCMulXAddC_apply, ExteriorAlgebra.GradedAlgebra.liftι_eq, 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, comp_toRingHom, Polynomial.expand_contract, AnalyticOn.aeval_polynomial, PowerBasis.exists_eq_aeval, Polynomial.algebraMap_pi_eq_aeval, 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ₐ, coe_toRingHom, Matrix.pow_eq_aeval_mod_charpoly, IntermediateField.algHomEquivAlgHomOfSplits_apply_apply, WeierstrassCurve.Jacobian.baseChange_add, Polynomial.derivWithin_aeval, coe_ringHom_injective, eval_minpolyDiv_self, MvPolynomial.eval₂_expand, Polynomial.disjoint_ker_aeval_of_isCoprime, MvPolynomial.universalFactorizationMap_comp_map, MvPolynomial.aeval_algebraMap_eq_zero_iff, MvPowerSeries.support_expand, PolynomialModule.smul_def, IsAdjoinRoot.mem_ker_map, ker_coe, PowerSeries.coeff_expand_mul, Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, eval₂_minpolyDiv_self, MvPolynomial.expand_X, 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', WittVector.ghostComponent_apply, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm, aeval_wittPolynomial, RatFunc.laurent_X, toRingHom_toRatAlgHom, WeierstrassCurve.Projective.baseChange_negDblY, NumberField.InfinitePlace.IsUnramified.comap_algHom, 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, AddMonoidAlgebra.mapRangeAlgHom_single, TensorProduct.toIntegralClosure_bijective_of_isLocalization, Polynomial.mem_rootSet_of_injective, Algebra.TensorProduct.mapOfCompatibleSMul_surjective, Polynomial.aeval_map_algebraMap, TensorAlgebra.toTrivSqZeroExt_ι, MonoidAlgebra.algHom_ext'_iff, eval₂_minpolyDiv_of_eval₂_eq_zero, MvPowerSeries.trunc'_expand_trunc', WeierstrassCurve.baseChange_preΨ, Algebra.lmul_algebraMap, comp_algebraMap, Unitization.splitMul_apply, minpoly.eq_iff_aeval_eq_zero, 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, DoubleQuot.coe_quotQuotMkₐ, Polynomial.coeff_zero_of_isScalarTower, WeierstrassCurve.Jacobian.baseChange_polynomialZ, FreeAlgebra.lift_comp_ι, 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, coe_mk, coe_mapIntegralClosure, AlgebraicIndependent.polynomial_aeval_of_transcendental, MvPowerSeries.mapAlgHom_apply, algHomClass, MvPolynomial.algHom_ext'_iff, IntermediateField.mem_adjoin_iff, RatFunc.laurent_algebraMap, AlgebraicIndependent.repr_ker, IsArithFrobAt.mk_apply, DoubleQuot.coe_quotLeftToQuotSupₐ, MvPolynomial.aeval_X, Rep.to_Module_monoidAlgebra_map_aux, AdicCompletion.val_smul_eq_evalₐ_smul, CliffordAlgebra.op_reverse, AlgCat.forget_obj, 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, MvPolynomial.optionEquivLeft_apply, 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, isConjRoot_algHom_iff, coe_coe, RatFunc.laurent_div, CliffordAlgebraQuaternion.toQuaternion_ofQuaternion, 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, Bialgebra.counitAlgHom_apply, Subalgebra.aeval_coe, CliffordAlgebraComplex.ofComplex_toComplex, MvPolynomial.ACounit_surjective, AddMonoidAlgebra.lift_mapRangeRingHom_algebraMap, WeierstrassCurve.Projective.baseChange_negY, UniversalEnvelopingAlgebra.lift_unique, RingQuot.mkAlgHom_surjective, DoubleQuot.quotQuotEquivComm_symmₐ, Ideal.Quotient.coe_factorₐ, Polynomial.aeval_iterate_derivative_self, MvPolynomial.aeval_eq_eval, PowerSeries.coeff_heval, Module.endTensorEndAlgHom_apply, MvPolynomial.aeval_ite_mem_eq_self, CliffordAlgebra.toProd_ι_tmul_one, coe_fn_inj, RingCon.quotientKerEquivRangeₐ_comp_mkₐ, Polynomial.mapAlgHom_eq_eval₂AlgHom'_CAlgHom, Algebra.TensorProduct.comm_comp_map_apply, MvPolynomial.eval₂Hom_C_id_eq_join₁, PowerSeries.aeval_eq_sum, PolyEquivTensor.toFunAlgHom_apply_tmul, PolynomialLaw.exists_lift', CliffordAlgebra.commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_right, MvPolynomial.eval_rename_prod_mk, AdjoinRoot.algHom_ext_iff, PowerBasis.equivAdjoinSimple_symm_aeval, TrivSqZeroExt.map_inr, MvPolynomial.aevalTower_comp_C, Polynomial.toAddCircle_X_pow_eq_fourier, Subalgebra.val_apply, MvPolynomial.rename_msymm, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd, coe_range, RingHom.toRatAlgHom_apply, IsAlgebraic.algHom, MvPolynomial.eval₂Hom_C_eq_bind₁, gelfandTransform_bijective, coe_id, Polynomial.differentiableOn_aeval, transcendental_iff_injective, Algebra.TensorProduct.map_tmul, op_apply_apply, coe_ringHom_mk, TensorProduct.toIntegralClosure_bijective_of_smooth, MvPolynomial.rename_id_apply, Algebra.toMatrix_lmul_eq, IsCyclotomicExtension.aeval_zeta, MvPowerSeries.expand_mul, Ideal.comap_idₐ, Ideal.Quotient.factorₐ_apply_mk, Algebra.IsAlgebraic.algHom_bijective, Polynomial.bernoulli_generating_function, 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, IsFractionRing.algHom_commutes, CommAlgCat.ofHom_apply, DualNumber.lift_apply_eps, AdjoinRoot.Minpoly.toAdjoin.surjective, Algebra.TensorProduct.includeRight_apply, Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat, Polynomial.aeval_X_pow, extendScalarsOfSurjective_apply, Polynomial.Bivariate.aveal_eq_map_swap, WeierstrassCurve.baseChange_Ψ₂Sq, IsLocalizedModule.map_linearMap_of_isLocalization, 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, 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, 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, AdicCompletion.factor_eval_eq_evalₐ, Subalgebra.range_isScalarTower_toAlgHom, FractionalIdeal.mem_map, Ideal.Quotient.factorₐ_apply, Polynomial.aeval_one, Algebra.Extension.CotangentSpace.map_tmul, Polynomial.aeval_eq_zero_of_mem_rootSet, Unitization.lift_symm_apply_apply, MvPolynomial.coeff_expand_smul, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, Algebra.Generators.algebraMap_apply, RingHom.toIntAlgHom_apply, Algebra.discr_powerBasis_eq_norm, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, QuaternionAlgebra.Basis.j_compHom, WeierstrassCurve.baseChange_preΨ', Polynomial.expand_one, MvPolynomial.expand_C, Algebra.toRingHom_ofId, WeierstrassCurve.Affine.baseChange_negY, TensorAlgebra.toExterior_ι, DoubleQuot.quotQuotToQuotSupₐ_toRingHom, Polynomial.aeval_subalgebra_coe, 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, CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd, WeierstrassCurve.baseChange_ψ₂, SkewMonoidAlgebra.lift_of, 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, 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, AddMonoidAlgebra.decomposeAux_coe, Polynomial.monic_mapAlg_iff, CommAlgCat.algEquivOfIso_apply, WeierstrassCurve.Projective.baseChange_polynomial, StarAlgHom.coe_mk', AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, UniversalEnvelopingAlgebra.ι_comp_lift, 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, 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', NonUnitalSubsemiring.unitization_apply, PowerBasis.leftMulMatrix, MonoidAlgebra.toRingHom_mapRangeAlgHom, CategoryTheory.Iso.toAlgEquiv_symm_apply, MvPolynomial.support_rename_of_injective, MonoidAlgebra.scalarTensorEquiv_tmul, MvPolynomial.ACounit_C, Polynomial.expand_C, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, CommAlgCat.algEquivOfIso_symm_apply, Polynomial.aevalTower_toAlgHom, comp_apply, IsAdjoinRootMonic.map_modByMonic, MvPolynomial.algebraicIndependent_polynomial_aeval_X, PowerSeries.substAlgHom_X, 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, spinGroup.units_involute_act_eq_conjAct, AddMonoidAlgebra.tensorEquiv.invFun_tmul, PowerSeries.expand_one_apply, 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, TensorAlgebra.equivDirectSum_apply, Algebra.Presentation.comp_aeval_relation_inl, AdjoinRoot.aeval_eq_of_algebra, RatFunc.laurent_at_zero, WittVector.mulN_coeff, Matrix.isRepresentation.toEnd_represents, DualNumber.lift_inlAlgHom_eps, StandardEtalePair.HasMap.map, BialgHom.coe_toAlgHom, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, QuadraticAlgebra.lift_apply_apply, 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, 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, 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, coe_prod, Algebra.TensorProduct.lmul'_apply_tmul, TensorAlgebra.lift_ι_apply, MvPowerSeries.HasSubst.comp, AddMonoidAlgebra.lift_apply, minpoly.dvd_iff, Algebra.TensorProduct.includeLeft_injective, toLinearMap_apply, galLift_algebraMap_apply, Algebra.Generators.toAlgHom_ofComp_surjective, comap_ker, 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, coe_toMonoidHom, ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf, IntermediateField.adjoin_map, CommAlgCat.lift_unop_hom, RingCon.kerLiftₐ_mk, map_adjugate, map_mem_separableClosure_iff, MvPolynomial.aeval_expand, DirectSum.toAlgebra_apply, liftOfDerivationToSquareZero_mk_apply, 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, 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, opComm_apply_apply, CliffordAlgebraComplex.ofComplex_I, IsArithFrobAt.localize_algebraMap, ker_rangeRestrict, AlgEquiv.ofAlgHom_symm_apply, Subalgebra.mvPolynomial_aeval_coe, 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, LocallyConstant.constₐ_apply_apply, PowerBasis.equivAdjoinSimple_aeval, traceForm_dualSubmodule_adjoin, WittVector.mul_polyOfInterest_aux4, AlgCat.forget_preservesLimits, MvPolynomial.rename_eval₂, IsArithFrobAt.apply_of_pow_eq_one, MvPowerSeries.expand_eq_expand, WeierstrassCurve.baseChange_φ, MvPowerSeries.substAlgHom_comp_substAlgHom_apply, IsAdjoinRootMonic.modByMonicHom_map, Polynomial.sup_aeval_range_eq_top_of_isCoprime, Algebra.FiniteType.iff_quotient_mvPolynomial', Algebra.TensorProduct.includeRight_injective, spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots, StarAlgHom.coe_toAlgHom, CliffordAlgebraQuaternion.equiv_symm_apply, map_det, WeierstrassCurve.Jacobian.baseChange_dblX, mulLeftRight_apply, WeierstrassCurve.Jacobian.baseChange_negDblY, 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, toKerIsLocalization_apply, MvPolynomial.aeval_bind₁, Polynomial.isCoprime_expand, CliffordAlgebraQuaternion.ofQuaternion_star, MonoidAlgebra.lift_unique, HomogeneousLocalization.awayMapₐ_apply, MvPolynomial.exists_fin_rename, mem_range, galLiftEquiv_apply, AdicCompletion.factorₐ_evalₐ_one, comp_algebraMap_of_tower, Algebra.FiniteType.iff_quotient_freeAlgebra, Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits_apply_apply, mapMatrix_apply, transcendental_aeval_iff, Polynomial.Splits.aeval_eq_prod_aroots, MonoidAlgebra.lift_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, IsArithFrobAt.comap_eq, 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, Polynomial.expand_expand, Subalgebra.mulMap'_surjective, Polynomial.mapAlgHom_monomial, IsArithFrobAt.restrict_injective, WittVector.bind₁_wittMulN_wittPolynomial, BialgCat.forget₂_algebra_map, DoubleQuot.coe_quotQuotEquivQuotSupₐ, AnalyticWithinAt.aeval_polynomial, Subalgebra.mem_map, sum_embeddings_eq_finrank_mul, MvPolynomial.aevalTower_C, DirectSum.coeAlgHom_of, MvPolynomial.expand_one_apply, Complex.liftAux_apply_I, MvPolynomial.map_expand_pow_char, MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure, Polynomial.aeval_apply_smul_mem_of_le_comap, Pi.algHom_apply, WeakDual.CharacterSpace.toAlgHom_apply, FiniteField.frobeniusAlgEquivOfAlgebraic_symm_apply, 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, Matrix.isRepresentation.toEnd_exists_mem_ideal, Representation.asAlgebraHom_single_one, Algebra.Generators.Hom.toAlgHom_X, MvPolynomial.bind₁_rename, 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, WeierstrassCurve.baseChange_Φ, Algebra.adjoin_mem_exists_aeval, 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, Polynomial.isNilpotent_aeval_sub_of_isNilpotent_sub, Module.End.IsSemisimple.aeval, MvPowerSeries.trunc'_expand, fieldRange_toSubfield, MvPolynomial.coeff_rename_mapDomain, StandardEtalePair.lift_X, Algebra.lsmul_injective, LocallyConstant.coeFnAlgHom_apply, MvPolynomial.expand_injective, minpoly.aeval, Algebra.Presentation.aeval_val_relation, MonoidAlgebra.isLocalHom_singleOneAlgHom, QuaternionAlgebra.Basis.i_compHom, MvPolynomial.esymmAlgHom_fin_surjective, MvPolynomial.expand_inj, mul_apply, Algebra.TensorProduct.includeRight_bijective, UniversalEnvelopingAlgebra.lift_ι_apply, Algebra.Generators.H1Cotangent.δAux_ofComp, TrivSqZeroExt.inlAlgHom_apply, Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, one_apply, PiTensorProduct.singleAlgHom_apply, Polynomial.int_eval₂_eq, AdjoinRoot.liftAlgHom_eq_algHom, CommRingCat.toAlgHom_apply, WeierstrassCurve.Jacobian.baseChange_dblU, 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, default_apply, Polynomial.algEquivAevalNegX_symm_apply, 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, GradedTensorProduct.includeRight_apply, 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, IsArithFrobAt.le_comap, Polynomial.aeval_mul, MvPolynomial.totalDegree_expand, map_adjoin, MvPolynomial.algHom_C, AddMonoidAlgebra.lift_symm_apply, StandardEtalePresentation.toSubmersivePresentation_jacobian, IsAlgClosed.exists_aeval_eq_zero_of_injective, Algebra.IsAlgebraic.algHom_bijective₂, wittStructureInt_prop, Polynomial.expand_eq_zero, Polynomial.differentiableAt_aeval, Submodule.coe_mulMap_comp_eq, 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_ι, Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splits, compLeft_apply, snd_apply, LinearMap.aeval_eq_aeval_mod_charpoly, 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ₐ, Algebra.smulTower_leftMulMatrix, MvPowerSeries.expand_subst, Module.Finite.exists_free_surjective, galRestrictHom_symm_algebraMap_apply, MvPolynomial.universalFactorizationMapPresentation_relation, AnalyticAt.aeval_polynomial, MvPolynomial.aevalTower_comp_algebraMap, 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, AdjoinRoot.Minpoly.coe_toAdjoin_mk_X, MvPolynomial.aeval_id_rename, Polynomial.expand_zero, CliffordAlgebraQuaternion.ofQuaternion_mk, WeierstrassCurve.Projective.baseChange_dblZ, Polynomial.roots_expand_pow_map_iterateFrobenius_le, PowerBasis.equivOfMinpoly_aeval, Algebra.Generators.aeval_val_σ, Subalgebra.algebraMap_eq, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ, MvPolynomial.mem_zeroLocus_iff, Polynomial.rootMultiplicity_expand, NonUnitalSubalgebra.unitization_apply, tensorEqualizerEquiv_apply, DualNumber.lift_apply_apply, Algebra.ofId_apply, WeierstrassCurve.Affine.baseChange_addPolynomial, Unitization.lift_symm_apply, transcendental_iff_ker_eq_bot, MonoidAlgebra.tensorEquiv_tmul, 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, MvPowerSeries.substAlgHom_coe, RingCon.quotientQuotientEquivQuotientₐ_mk_mk, CliffordAlgebra.evenToNeg_ι, MvPolynomial.coeff_rTensorAlgHom_tmul, FiniteGaloisIntermediateField.adjoin_map, Representation.asAlgebraHom_of, MvPolynomial.aeval_zero, WeierstrassCurve.baseChange_Ψ, Algebra.leftMulMatrix_complex, MvPolynomial.killCompl_rename_app, diffToIdealOfQuotientCompEq_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, IntermediateField.mem_adjoin_range_iff, CommAlgCat.forget₂_algCat_obj, SymmetricAlgebra.lift_comp_ι, WittVector.coeff_frobeniusFun, 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_ι, WeierstrassCurve.Jacobian.baseChange_neg, Polynomial.hasDerivWithinAt_aeval, Polynomial.aeval_coe_eq_smeval, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, Polynomial.IsMonicOfDegree.aeval_add, AlgebraicClosure.toSplittingField_coeff, Polynomial.hasStrictDerivAt_aeval, Algebra.embeddingsMatrix_apply, RestrictScalars.lsmul_apply_apply, Subalgebra.coe_val, Polynomial.aeval_algebraMap_eq_zero_iff_of_injective, toUnder_right, StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x, liftNormal_commutes, ExteriorAlgebra.map_injective, coe_mks, CommAlgCat.forget_obj, IsAdicComplete.mk_liftAlgHom, 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, coe_comp, Subalgebra.coe_map, Polynomial.monic_expand_iff, Polynomial.natSepDegree_expand, Polynomial.toAddCircle_monomial_eq_smul_fourier, algebraicIndependent_iff_injective_aeval, MvPolynomial.aeval_map_algebraMap, Algebra.Generators.Hom.toAlgHom_C, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, coe_fieldRange, Subalgebra.LinearDisjoint.linearIndependent_right_of_flat, Matrix.diagonalAlgHom_apply, Algebra.smul_units_def, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ, congr_arg, MvPolynomial.coeToMvPowerSeries.algHom_apply, IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk, AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc, AlgebraicIndependent.liftAlgHom_comp_reprField, AlgCat.forget₂_module_obj, sectionOfRetractionKerToTensor_algebraMap, MvPolynomial.rename_rightInverse, RingCon.mkₐ_apply, LinearMap.aeval_self_charpoly, WeierstrassCurve.Projective.baseChange_add, Polynomial.rootSet_maps_to', coe_ideal_map, coe_restrictScalars', 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, AddMonoidAlgebra.toRingHom_mapRangeAlgHom, 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, 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, UniversalEnvelopingAlgebra.ι_apply, Polynomial.algHom_ext_iff, Polynomial.coeToPowerSeries.algHom_apply, AdicCompletion.evalOneₐ_of, PowerBasis.equivOfMinpoly_apply, CommAlgCat.forget_map, WeierstrassCurve.map_baseChange, eqOn_adjoin_iff, map_smul_of_tower, CliffordAlgebra.prodEquiv_symm_apply, MvPowerSeries.expand_monomial, MvPolynomial.aeval_bind₂, MvPolynomial.rename_bind₁, 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, Polynomial.map_expand_pow_char, CliffordAlgebra.involute_ι, 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, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, not_irreducible_expand, AddMonoidAlgebra.lift_of', liftOfDerivationToSquareZero_apply, Derivation.tensorProductTo_mul, fieldRange_eq_top, 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, FreeAlgebra.lift_unique, subalgebraMap_coe_apply, WeierstrassCurve.Jacobian.baseChange_dblXYZ, Polynomial.coeff_zero_eq_aeval_zero, CliffordAlgebra.prodEquiv_apply, 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, 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.evenEquivEvenNeg_apply, Polynomial.fourierCoeff_toAddCircle_natCast, Subalgebra.linearDisjoint_iff_injective, QuadraticAlgebra.algHom_ext_iff, spectrum.map_polynomial_aeval_of_degree_pos, mem_fieldRange, Algebra.Generators.repr_CotangentSpaceMap, MonoidAlgebra.lift_apply, Polynomial.annIdealGenerator_aeval_eq_zero, DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ, MonoidAlgebra.lift_mapRangeRingHom_algebraMap, isNilpotent_tensor_residueField_iff, Polynomial.toContinuousMapAlgHom_apply, 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, StandardEtalePresentation.toPresentation_σ', toRingHom_eq_coe, witt_structure_prop, Derivation.map_aeval, WeierstrassCurve.Jacobian.Equation.baseChange, CliffordAlgebra.toEven_ι, Polynomial.Splits.aeval_eq_prod_aroots_of_monic, PolyEquivTensor.left_inv, CliffordAlgebra.equivBaseChange_apply, LinearMap.toMvPolynomial_comp, 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, PowerSeries.map_expand, 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, Polynomial.rootsExpandToRoots_apply, RingQuot.mkAlgHom_rel, StandardEtalePair.HasMap.isUnit_derivative_f, 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, Polynomial.expand_eq_C, MvPolynomial.aeval_unique, WeierstrassCurve.Jacobian.baseChange_polynomialX, Polynomial.aeval_C, PowerBasis.exists_eq_aeval', Algebra.toMatrix_lsmul, Polynomial.aeval_eq_prod_aroots_sub_of_splits, MvPolynomial.coeff_rTensorAlgHom_monomial_tmul, MvPolynomial.bind₁_bind₁, TensorProduct.toIntegralClosure_injective_of_flat, Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime, AdicCompletion.mk_ofAlgEquiv_symm_eq_evalOneₐ, Algebra.TensorProduct.productMap_right_apply, Module.End.baseChangeHom_apply_apply, MvPolynomial.rename_polynomial_aeval_X, MvPolynomial.coeff_expand_of_not_dvd, Matrix.isRepresentation.toEnd_surjective, Polynomial.comp_eq_aeval, Algebra.Generators.Hom.equivAlgHom_symm_apply_val, Polynomial.valuation_aeval_monomial_eq_valuation_pow, MvPolynomial.map_iterateFrobenius_expand, Polynomial.toMvPolynomial_X, MvPowerSeries.coe_aeval, Polynomial.aeval_ofReal, AddMonoidAlgebra.algHom_ext_iff, Algebra.Generators.ker_comp_eq_sup, map_mem_algebraicClosure_iff, Polynomial.hasDerivAt_aeval, WeierstrassCurve.Projective.baseChange_dblX, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, Polynomial.Chebyshev.aeval_C, Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply, Polynomial.aeval_eq_sum_range, polyEquivTensor_apply, MvPolynomial.exists_finset_rename₂, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply, WeierstrassCurve.Projective.baseChange_dblU, MvPolynomial.eval_toMvPolynomial, AlgCat.forget₂Module_preservesLimits, 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, addHomMk_coe, MvPolynomial.aeval_eq_eval₂Hom, DoubleQuot.quotQuotEquivCommₐ_toRingEquiv, DoubleQuot.coe_quotQuotToQuotSupₐ, 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, MvPowerSeries.map_frobenius_expand, MvPolynomial.transcendental_polynomial_aeval_X, AlgebraicIndependent.aevalEquiv_apply_coe, MvPolynomial.rename_C, MvPowerSeries.expand_X, commutes, MvPowerSeries.map_expand, subalgebraMap_surjective, Algebra.Extension.Hom.sub_aux, StandardEtalePresentation.aeval_val_equivMvPolynomial, Ideal.map_mapₐ, Module.Basis.localizationLocalization_span, Polynomial.mem_rootSet', congr_fun, PowerSeries.HasSubst.comp, CliffordAlgebra.reverseOp_ι, bijective, map_coe_real_complex, MvPolynomial.IsHomogeneous.rename_isHomogeneous, ExteriorAlgebra.algebraMap_leftInverse, Algebra.norm_apply, DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv, WittVector.polyOfInterest_vars_eq, coe_fn_injective, AlgCat.comp_apply, NormedAlgebra.Real.exists_isMonicOfDegree_two_and_aeval_eq_zero, IsAdjoinRoot.algebraMap_apply, BoundedContinuousFunction.coe_toContinuousMapₐ, StandardEtalePair.aeval_X_g_mul_mk_X, MvPolynomial.pderiv_inr_universalFactorizationMap_X, TrivSqZeroExt.fst_map, Transcendental.aeval, MvPowerSeries.constantCoeff_expand, Representation.ofModule_asAlgebraHom_apply_apply, TensorAlgebra.equivDirectSum_symm_apply, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, PowerSeries.continuous_aeval, Algebra.Generators.ker_eq_ker_aeval_val, Polynomial.aeval_endomorphism, IntermediateField.coe_equivMap_apply, IntermediateField.mem_adjoin_simple_iff, Matrix.isRepresentation.eq_toEnd_of_represents, PowerSeries.heval_unit, sectionOfRetractionKerToTensorAux_algebraMap, IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe, SymmetricAlgebra.algHom_surjective, Algebra.baseChange_lmul, WeakDual.gelfandTransform_apply_apply, Polynomial.expand_contract', Module.AEval.of_aeval_smul, Algebra.mem_ideal_map_adjoin, Polynomial.mem_aroots, WeierstrassCurve.Affine.Point.map_some, ZMod.expand_card, MvPolynomial.aeval_C_comp_left, Subalgebra.LinearDisjoint.linearIndependent_left_of_flat_of_commute, IsAdjoinRoot.map_self, Algebra.leftMulMatrix_mulVec_repr, ExteriorAlgebra.map_apply_ιMulti, IsLocalization.mapₐ_coe, AlgCat.forget_reflects_isos, MvPolynomial.degrees_rename_of_injective, restrictScalars_apply, LieRinehartAlgebra.Hom.map_smul_apply, PowerBasis.liftEquiv'_apply_coe, MvPolynomial.mapAlgHom_apply, Algebra.Generators.cotangentRestrict_mk, minpoly.coe_equivAdjoin, CliffordAlgebra.toProd_one_tmul_ι, MvPowerSeries.substAlgHom_monomial, CliffordAlgebra.toBaseChange_involute, Polynomial.algEquivAevalNegX_apply, WittVector.bind₁_onePoly_wittPolynomial, 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, 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, MvPolynomial.comap_apply, IsAdjoinRoot.map_eq_zero_iff, MulSemiringAction.toAlgHom_apply, MvPolynomial.vars_rename, CommRingCat.Under.equalizerFork_ι, WittVector.bind₁_zero_wittPolynomial, Polynomial.exists_separable_of_irreducible, Polynomial.roots_expand_image_iterateFrobenius, IntermediateField.val_mk, DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv, MatrixEquivTensor.right_inv, 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, normal_bijective, StandardEtalePresentation.toPresentation_val, Polynomial.algEquivOfCompEqX_apply, Polynomial.mem_rootSet_of_ne, Polynomial.mapAlg_comp, IsAdjoinRoot.aeval_root_self, RingHom.toIntAlgHom_coe, Polynomial.aeval_eq_sum_range', MvPolynomial.rename_comp_bind₁, Polynomial.expand_char, Polynomial.aeval_zero, 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, Polynomial.roots_expand_pow_image_iterateFrobenius_subset, AlgEquiv.ofAlgHom_apply, 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, AdicCompletion.evalOneₐ_surjective, 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, AdicCompletion.evalₐ_comp_liftRingHom, isAlgebraic_iff_not_injective, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, CliffordAlgebraComplex.toComplex_ofComplex, MvPolynomial.aeval_sumElim_pderiv_inl, FiniteField.expand_card, AnalyticAt.aeval_mvPolynomial, map_algebraMap, Polynomial.coeff_expand_mul', Polynomial.differentiableWithinAt_aeval, Unitization.norm_splitMul_snd_sq, AdjoinRoot.coe_algEquivOfEq, ContinuousMap.evalAlgHom_apply, WeakDual.CharacterSpace.equivAlgHom_coe, AlgCat.forget₂Ring_preservesLimits, AdjoinRoot.aeval_eq, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, Polynomial.coeff_zero_eq_aeval_zero', MvPolynomial.isSymmetric_rename, CliffordAlgebra.ofEven_ι, CliffordAlgebra.ofBaseChange_tmul_one, Polynomial.roots_expand_pow, MvPolynomial.universalFactorizationMap_freeMonic, map_adjoin_singleton, Subalgebra.toSubring_subtype, AnalyticOnNhd.aeval_polynomial, Algebra.Generators.Hom.toAlgHom_monomial, DualNumber.lift_apply_inl, MvPolynomial.coe_expand, Polynomial.contract_mul_expand, Polynomial.algEquivAevalXAddC_apply, MvPolynomial.aeval_sumElim, Polynomial.map_frobenius_expand, Unitization.splitMul_injective, AddMonoidAlgebra.decomposeAux_single, DualNumber.lift_op_smul, MvPolynomial.eval₂_rename_prod_mk, 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, Ideal.KerLift.map_smul, Polynomial.coe_aeval_eq_eval, Algebra.FinitePresentation.out, Matrix.aeval_self_charpoly, toRingHom_toAddMonoidHom, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, ContinuousMap.compRightAlgHom_continuous, MvPolynomial.rename_leftInverse, PowerBasis.liftEquiv'_symm_apply_apply, IsArithFrobAt.restrict_mk, AdicCompletion.evalₐ_mkₐ, Algebra.FiniteType.iff_quotient_mvPolynomial'', Algebra.TensorProduct.includeRight_surjective, MvPolynomial.esymmAlgHom_fin_bijective, RingHom.toNatAlgHom_apply, IsLocalization.Away.mapₐ_apply, MvPolynomial.esymmAlgEquiv_apply, PowerSeries.aeval_coe, MvPolynomial.mem_vanishingIdeal_iff, MvPolynomial.mem_vanishingIdeal_singleton_iff, gelfandTransform_isometry, Quaternion.coe_ofComplex, MonoidAlgebra.singleOneAlgHom_apply, Submodule.coe_mapAlgHom_apply, 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, Polynomial.Monic.expand, MvPolynomial.aeval_zero', MvPolynomial.weightedTotalDegree_rename_of_injective, Polynomial.aeval_iterate_derivative_of_lt, WeierstrassCurve.Projective.baseChange_polynomialZ, PowerSeries.substAlgHom_coe, linearMapMk_toAddHom, 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₁, MvPolynomial.degreeOf_eq_natDegree, 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, toRingHom_toMonoidHom, Complex.ofRealAm_coe, WeierstrassCurve.Affine.baseChange_polynomialY, Algebra.smulTower_leftMulMatrix_algebraMap_eq, lipschitzGroup.involute_act_ι_mem_range_ι, WeierstrassCurve.Affine.baseChange_addX, Polynomial.aeval_algHom_apply, Polynomial.coe_toLaurentAlg, WittVector.mul_polyOfInterest_aux3, AddMonoidAlgebra.scalarTensorEquiv_tmul, Polynomial.shiftedLegendre_eval_symm, Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits, MvPolynomial.aeval_prod, RatFunc.aeval_X_left_eq_algebraMap, Matrix.toMvPolynomial_mul, Subalgebra.toSubsemiring_subtype, MvPolynomial.exists_restrict_to_vars, wittStructureInt_rename, restrictNormal_commutes, TrivSqZeroExt.fstHom_apply, Polynomial.mapAlgHom_coe_ringHom, MvPolynomial.aevalTower_algebraMap, Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor, Polynomial.expand_aeval, PowerSeries.substAlgHom_comp_substAlgHom_apply, id_toRingHom, Subalgebra.mulMap_tmul, RingCon.liftₐ_mk, WeierstrassCurve.Jacobian.baseChange_negY, BialgCat.forget₂_algebra_obj, Polynomial.aeval_natCast, kerSquareLift_mk, trace_eq_sum_embeddings_gen, MvPolynomial.eval_expand, 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, RingCon.coe_liftₐ, Polynomial.toLaurentAlg_apply, FiniteField.coe_frobeniusAlgHom, Algebra.IsAlgebraic.bijective_of_isScalarTower, WeierstrassCurve.Projective.baseChange_dblY, MonoidAlgebra.mapDomainAlgHom_apply, Pi.evalAlgHom_apply, TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι, AlgebraicGeometry.pullbackSpecIso_hom_snd, Subalgebra.map_toSubsemiring, spectrum.map_polynomial_aeval, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, spinGroup.involute_eq, DoubleQuot.quotLeftToQuotSupₐ_toRingHom, Algebra.Extension.Cotangent.map_mk, MatrixEquivTensor.toFunAlgHom_apply, PowerSeries.heval_mul, Polynomial.toAddCircle_C_eq_smul_fourier_zero, 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, MvPolynomial.aeval_natDegree_le, 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, op_symm_apply_apply, toLieHom_apply, DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv, WittVector.coeff_frobenius, Matrix.aeval_eq_aeval_mod_charpoly, RingCon.quotientQuotientEquivQuotientₐ_coe_coe, Polynomial.aeval_algebraMap_apply, Algebra.Generators.comp_σ, CliffordAlgebraQuaternion.toQuaternion_ι, 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, MvPolynomial.coe_aeval_eq_eval, FreeAlgebra.hom_ext_iff, BialgCat.MonoidalCategory.inducingFunctorData_εIso, FreeAlgebra.algebraMap_leftInverse, 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, toFun_eq_coe, MvPowerSeries.substAlgHom_apply, prod_apply, WeierstrassCurve.Affine.baseChange_negAddY, ContinuousMap.compRightAlgHom_apply, AdjoinRoot.algHomOfDvd_apply_root, Module.AEval.annihilator_eq_ker_aeval, Ideal.map_includeLeft_eq, Polynomial.aeval_add, Polynomial.continuousOn_aeval, CliffordAlgebra.equivOfIsometry_apply, MvPowerSeries.substAlgHom_comp_substAlgHom, Polynomial.aeval_sub, 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, Polynomial.exists_monic_aeval_eq_zero_forall_mem_of_mem_map, 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, CliffordAlgebra.leftInverse_map_of_leftInverse, AdjoinRoot.mkₐ_toRingHom, Matrix.mvPolynomialX_mapMatrix_aeval, IsAdjoinRoot.algEquiv_apply_map, range_toSubsemiring, Polynomial.roots_expand_map_frobenius_le, AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective, AdicCompletion.evalₐ_liftRingHom, coe_toAddMonoidHom, CliffordAlgebra.EquivEven.involute_v, Polynomial.aeval_homogenize_of_eq_one, MonoidAlgebra.lift_single, AddMonoidAlgebra.mapRangeAlgHom_apply, Polynomial.toContinuousMapOnAlgHom_apply, 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, WeierstrassCurve.Jacobian.baseChange_negAddY, IntermediateField.coe_map, MvPolynomial.mapEquivMonic_symm_map, Algebra.SubmersivePresentation.basisDeriv_apply, MvPolynomial.bind₁_monomial, RingCon.coe_quotientKerEquivRangeₐ_mkₐ, LocallyConstant.toContinuousMapAlgHom_apply, Ideal.kerLiftAlg_mk, UniversalEnvelopingAlgebra.lift_ι_apply', Algebra.TensorProduct.linearEquivIncludeRange_tmul, RingQuot.eq_liftAlgHom_comp_mkAlgHom, Algebra.lsmul_coe, 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, CommRingCat.Under.equalizer_comp, coe_pow, IsScalarTower.toAlgHom_apply, Polynomial.map_iterateFrobenius_expand, retractionOfSectionOfKerSqZero_tmul_D, MvPolynomial.rename_surjective, AlgCat.instIsRightAdjointForgetAlgHomCarrier, Polynomial.eval₂_algebraMap_X, 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, coe_monoidHom_injective, RingQuot.mkAlgHom_coe, MonoidAlgebra.lift_of, cfc_comp_polynomial, MvPolynomial.esymmAlgHom_injective, MvPolynomial.expand_zero_apply, Polynomial.expand_pow, PowerBasis.liftEquiv_apply_coe, IsAzumaya.AlgHom.mulLeftRight_bij, 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, Polynomial.aeval_sumIDeriv_of_pos, Polynomial.continuousWithinAt_aeval, CliffordAlgebraQuaternion.ofQuaternion_toQuaternion, MvPolynomial.pderiv_inl_universalFactorizationMap_X, SkewMonoidAlgebra.lift_symm_apply, 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
id 📖	CompOp	117 math math: CommRingCat.tensorProd_map_right, CliffordAlgebra.map_id, Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_right, MvPolynomial.aeval_X_left, TrivSqZeroExt.lift_inlAlgHom_inrHom, Complex.real_algHom_eq_id_or_conj, ContinuousAlgHom.coe_id, ContinuousAlgHom.coe_eq_id, Subalgebra.centralizer_coe_map_includeLeft_eq_center_tensorProduct, CliffordAlgebra.toProd_comp_ofProd, MvPolynomial.killCompl_comp_rename, toLieHom_id, CliffordAlgebraComplex.toComplex_comp_ofComplex, MvPolynomial.comap_id, Algebra.ofId_self, coe_id, AddMonoidAlgebra.mapDomainAlgHom_id, galRestrict'_id, Ideal.comap_idₐ, MvPolynomial.bind₁_X_left, CliffordAlgebra.toBaseChange_comp_ofBaseChange, MvPolynomial.mapAlgHom_id, toAlgHom_comp_sectionOfRetractionKerToTensorAux, CliffordAlgebra.toBaseChange_comp_involute, Ideal.Quotient.factorₐ_refl, id_comp, Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProduct, CommAlgCat.ofHom_id, DualNumber.lift_inlAlgHom_eps, MonoidAlgebra.mapDomainAlgHom_id, KaehlerDifferential.End_equiv_aux, coe_tensorEqualizer, Polynomial.aeval_X_left, Algebra.FiniteType.baseChangeAux_surj, MvPowerSeries.rescaleAlgHom_one, CliffordAlgebra.involute_comp_involute, Bialgebra.counitAlgHom_self, Subalgebra.centralizer_coe_map_includeRight_eq_center_tensorProduct, Algebra.TensorProduct.map_id, Complex.liftAux_I, CommRingCat.toAlgHom_id, CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion, MvPowerSeries.expand_one, CliffordAlgebra.toEven_comp_ofEven, MvPolynomial.expand_one, FractionalIdeal.map_id, ofLinearMap_id, AlgEquiv.symm_comp, Finite.id, Algebra.TensorProduct.lmul'_comp_includeRight, Algebra.TensorProduct.map_comp_id, Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_left, AlgCat.hom_whiskerLeft, Pi.algHom_evalAlgHom, FinitePresentation.id, AlgCat.ofHom_id, Polynomial.aevalTower_id, tensorEqualizerEquiv_apply, Subalgebra.map_id, SymmetricAlgebra.lift_ι, CommAlgCat.whiskerLeft_hom, AlgEquiv.refl_toAlgHom, FiniteType.id, CommAlgCat.whiskerRight_hom, TensorAlgebra.toDirectSum_comp_ofDirectSum, Subalgebra.inclusion_self, IntermediateField.inclusion_self, mapMatrix_id, galLift_id, Algebra.FormallySmooth.iff_split_surjection, CliffordAlgebra.ofEven_comp_toEven, toAlgHom_comp_sectionOfRetractionKerToTensor, CliffordAlgebraRing.involute_eq_id, CommAlgCat.hom_id, CliffordAlgebra.ofProd_comp_toProd, prod_fst_snd, Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct, Submodule.mapHom_id, Algebra.TensorProduct.lTensor_ker, End_toOne_one, toLinearMap_id, AlgEquiv.comp_symm, Algebra.Generators.Hom.toAlgHom_id, PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable, Algebra.TensorProduct.lmul'_comp_includeLeft, ExteriorAlgebra.map_id, MvPolynomial.comap_id_apply, CliffordAlgebraQuaternion.ofQuaternion_comp_toQuaternion, comp_id, AlgCat.hom_id, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, PowerSeries.expand_one, StandardEtalePair.lift_X_left, Subalgebra.centralizer_coe_image_includeLeft_eq_center_tensorProduct, Ideal.map_idₐ, CliffordAlgebraComplex.ofComplex_comp_toComplex, Algebra.FormallySmooth.exists_kerProj_comp_eq_id, TensorAlgebra.ofDirectSum_comp_toDirectSum, id_toRingHom, Algebra.TensorProduct.map_id_comp, AlgCat.hom_whiskerRight, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, CommBialgCat.hom_id, MvPolynomial.aevalTower_id, CliffordAlgebra.evenToNeg_comp_evenToNeg, BialgHom.id_toAlgHom, IntermediateField.map_id, Algebra.range_id, Polynomial.mapAlgHom_id, CliffordAlgebra.ofBaseChange_comp_toBaseChange, Algebra.TensorProduct.rTensor_ker, Algebra.Extension.Hom.toAlgHom_id, Algebra.TensorProduct.lift_includeLeft_includeRight, TrivSqZeroExt.map_id, Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct, id_apply, MvPolynomial.rename_id
mk' 📖	CompOp	1 math math: coe_mk'
ofLinearMap 📖	CompOp	5 math math: toLinearMap_ofLinearMap, ofLinearMap_apply, ofLinearMap_id, LinearAlgebra.FreeProduct.ι_def, ofLinearMap_toLinearMap
toAddMonoidHom' 📖	CompOp	1 math math: AlgEquiv.algHomUnitsEquiv_apply_symm_apply
toEnd 📖	CompOp	1 math math: toEnd_apply
toLinearMap 📖	CompOp	109 math math: CliffordAlgebra.ι_range_map_map, coe_toLinearMap, Polynomial.lcoeff_comp_mapAlgHom_eq, Complex.ofRealCLM_coe, comp_toLinearMap, TensorAlgebra.ι_comp_lift, Ideal.span_pow_eq_map_homogeneousSubmodule, Ideal.span_eq_map_homogeneousSubmodule, toLinearMap_ofLinearMap, minpoly_algHom_toLinearMap, Subalgebra.mulMap_toLinearMap, mulLeftRightMatrix.inv_comp, PolynomialLaw.exists_lift', PolynomialLaw.toFun_eq_rTensor_φ_toFun', CliffordAlgebra.ι_range_map_lift, ExteriorAlgebra.map_comp_ι, toLinearMap_toOpposite, Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap, ExteriorAlgebra.map_comp_ιMulti, TrivSqZeroExt.lift_comp_inrHom, Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap, CliffordAlgebra.ι_comp_lift, CliffordAlgebra.lift_unique, TrivSqZeroExt.algHom_ext'_iff, Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap, ExteriorAlgebra.lift_comp_ι, Bialgebra.toLinearMap_counitAlgHom, TensorProduct.Algebra.exists_of_fg, comp_mul', linearIndependent_algHom_toLinearMap', TensorAlgebra.lift_symm_apply, AlgEquiv.toLinearMap_ofAlgHom, ExteriorAlgebra.ι_comp_lift, CliffordAlgebra.EvenHom.compr₂_bilin, linearIndependent_algHom_toLinearMap, linearIndependent_toLinearMap, TrivSqZeroExt.map_comp_inrHom, toLinearMap_apply, CliffordAlgebra.hom_ext_iff, PolynomialLaw.exists_lift, TensorAlgebra.lift_comp_ι, AlgEquiv.toAlgHom_toLinearMap, IsLocalization.mk'_algebraMap_eq_mk', isLocalizedModule_iff_isLocalization, Algebra.isPushout_iff, CliffordAlgebra.ι_range_map_involute, Algebra.IsAlgebraic.instIsLocalizedModuleNonZeroDivisorsToLinearMapToAlgHom, toLinearMap_injective, MvPolynomial.rTensorAlgHom_toLinearMap, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, CliffordAlgebra.ι_range_comap_involute, instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid, Submodule.map_mul, CliffordAlgebra.lift_symm_apply, DirectSum.algHom_ext'_iff, Algebra.IsPushout.out, LinearMap.rTensor_baseChange, Subalgebra.map_toSubmodule, CliffordAlgebra.map_comp_ι, PolynomialLaw.isCompat, TrivSqZeroExt.sndHom_comp_map, TensorAlgebra.hom_ext_iff, FractionalIdeal.coe_map, CliffordAlgebra.reverse_comp_involute, toLinearMap_fromOpposite, Algebra.IsAlgebraic.isBaseChange_of_isFractionRing, IsLocalization.map_eq_toLinearMap_mapₐ, Submodule.exists_fg_of_baseChange_eq_zero, CliffordAlgebra.even.lift_symm_apply_bilin, FiniteField.minpoly_frobeniusAlgHom, IsLocalizedModule.mkOfAlgebra, IsLocalization.mapExtendScalars_eq_toLinearMap_mapₐ, Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap, toLinearMap_id, CliffordAlgebra.evenOdd_map_involute, TrivSqZeroExt.liftEquivOfComm_symm_apply_coe, CliffordAlgebra.toBaseChange_involute, IsFractional.map, ExteriorAlgebra.lift_unique, AlgCat.forget₂_module_map, ExteriorAlgebra.hom_ext_iff, Submodule.map_pow, PolynomialLaw.isCompat_apply', IsLocalizedModule.mk'_mul_mk', ExteriorAlgebra.ιInv_comp_map, CliffordAlgebra.lift_comp_ι, LinearMap.algHom_comp_convMul_distrib, toEnd_apply, IsLocalization.map_linearMap_eq_toLinearMap_mapₐ, Submodule.mapHom_apply, LinearAlgebra.FreeProduct.lift_apply, PolynomialLaw.isCompat_apply, Algebra.TensorProduct.lmul'_toLinearMap, ExteriorAlgebra.ι_range_map_map, linearMapMk_toAddHom, Bialgebra.toLinearMap_comulAlgHom, DualNumber.algHom_ext'_iff, Algebra.FormallyUnramified.comp_sec, TensorAlgebra.lift_unique, ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom, CliffordAlgebra.evenOdd_comap_involute, TrivSqZeroExt.liftEquiv_symm_apply_coe, Algebra.TensorProduct.toLinearMap_map, RCLike.ofRealCLM_coe, Submodule.map_one, CliffordAlgebra.submodule_map_involute_eq_comap, PolynomialLaw.isCompat', mulLeftRightMatrix.comp_inv, TensorProduct.includeRight_lid
toMonoidHom' 📖	CompOp	—
toRingHom 📖	CompOp	115 math math: PrimeSpectrum.preimageEquivFiber_symm_apply_coe, MvPolynomial.universalFactorizationMap_comp_map, algebraicIndependent_iff_ker_eq_bot, LinearEquiv.algEquivOfRing_apply, AlgebraicGeometry.diagonal_SpecMap, Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul, Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, MvPolynomial.map_comp_rename, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, Subalgebra.inclusion.isScalarTower_left, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, commutes', Polynomial.Monic.quotient_isIntegral, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, MvPowerSeries.comp_aeval, IsFractionRing.coe_liftAlgHom, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, IsLocalization.coe_liftAlgHom, CommRingCat.pushoutCocone_inr, Algebra.SubmersivePresentation.ofSubsingleton_relation, MonoidAlgebra.toRingHom_mapRangeAlgHom, IsLocalization.liftAlgHom_apply, CommRingCat.coproductCocone_inl, Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap, PowerSeries.aeval_unique, Ideal.Quotient.mkₐ_toRingHom, KaehlerDifferential.End_equiv_aux, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, Algebra.FinitePresentation.ker_fg_of_mvPolynomial, RingCon.kerLiftₐ_mk, CommRingCat.isPushout_tensorProduct, AlgebraicIndependent.lift_reprField, CommRingCat.coproductCocone_inr, AddMonoidAlgebra.mapRangeAlgEquiv_apply, Ideal.quotientKerAlgEquivOfRightInverse_symm_apply, toKerIsLocalization_apply, Ideal.quotientKerAlgEquivOfRightInverse_apply, MonoidAlgebra.mapRangeAlgEquiv_apply, MvPolynomial.universalFactorizationMapPresentation_map, Localization.localAlgHom_apply, MvPowerSeries.comp_subst_apply, Algebra.FinitePresentation.ker_fG_of_surjective, exists_integral_inj_algHom_of_quotient, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, Algebra.algebraMapSubmonoid_le_comap, RingCon.kerLiftₐ_injective, ModuleCat.Algebra.instLinearRestrictScalars, Algebra.Generators.Hom.toExtensionHom_toRingHom, MvPolynomial.universalFactorizationMapPresentation_relation, Ideal.quotientKerAlgEquivOfSurjective_apply, RingCon.kerLiftₐ_range_eq, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, Subalgebra.inclusion.isScalarTower_right, AdjoinRoot.toRingHom_liftAlgHom, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, Algebra.Generators.self_algebra_smul, Subalgebra.inclusion.faithfulSMul, LinearMap.polyCharpolyAux_map_aeval, AddMonoidAlgebra.toRingHom_mapRangeAlgHom, Algebra.FormallySmooth.iff_split_surjection, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AdjoinRoot.coe_liftAlgHom, PowerSeries.comp_aeval, toRingHom_eq_coe, CommRingCat.coproductCoconeIsColimit_desc, Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime, IsFractionRing.liftAlgHom_toRingHom, toRingHom_unop, IsLocalization.liftAlgHom_toRingHom, AlgebraicIndependent.aevalEquivField_apply_coe, RingHom.Finite.tensorProductMap, Algebra.Generators.ker_ofAlgHom, toRingHom_op, WeierstrassCurve.Affine.Point.map_some, IsLocalization.mapₐ_coe, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, ker_kerSquareLift, PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable, MvPolynomial.finSuccEquiv_rename_finSuccEquiv, MvPolynomial.universalFactorizationMapPresentation_algebra_smul, IsLocalization.isLocalization_algebraMapSubmonoid_map_algHom, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, MvPowerSeries.comp_subst, MvPolynomial.universalFactorizationMapPresentation_val, isScalarTower_of_section_of_ker_sqZero, AlgebraicGeometry.diagonal_Spec_map, MvPolynomial.universalFactorizationMapPresentation_σ', Ideal.KerLift.map_smul, Algebra.FinitePresentation.out, IsLocalization.Away.mapₐ_apply, instRingHomCompTripleComp, RingHom.SurjectiveOnStalks.baseChange', ContinuousAlgHom.cont, Algebra.Generators.self_algebra_algebraMap, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, Algebra.TensorProduct.ringHom_ext_iff, kerSquareLift_mk, StarAlgHom.map_star', AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, MvPowerSeries.comp_substAlgHom, LieRinehartAlgebra.Hom.toLinearMap'_apply, minpoly.ker_eval, exists_integral_inj_algHom_of_fg, toFun_eq_coe, MvPowerSeries.aeval_unique, CommRingCat.coproductCocone_ι, Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, IsScalarTower.of_algHom, RingHom.equivRatAlgHom_symm_apply, AlgEquiv.algHomUnitsEquiv_apply_apply, MvPolynomial.universalFactorizationMapPresentation_jacobian, IsFractionRing.liftAlgHom_apply, Algebra.FinitePresentation.iff_quotient_mvPolynomial', Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
End_toOne_one 📖	mathematical	—	AlgHom Monoid.toOne End id	—	—
End_toSemigroup_toMul_mul 📖	mathematical	—	AlgHom Semigroup.toMul Monoid.toSemigroup End comp	—	—
addHomMk_coe 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe AlgHom funLike map_add SemilinearMapClass.toAddHomClass CommSemiring.toSemiring RingHom.id Algebra.toModule AlgHomClass.linearMapClass algHomClass AddHomClass.toAddHom	—	map_add SemilinearMapClass.toAddHomClass AlgHomClass.linearMapClass algHomClass
algHomClass 📖	mathematical	—	AlgHomClass AlgHom funLike	—	MonoidHom.map_mul' OneHom.map_one' RingHom.map_add' RingHom.map_zero' commutes'
algebraMap_eq_apply 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	AlgHom funLike	—	commutes
cancel_left 📖	mathematical	DFunLike.coe AlgHom funLike	comp	—	ext ext_iff
cancel_right 📖	mathematical	DFunLike.coe AlgHom funLike	comp	—	ext Function.Surjective.forall ext_iff
coe_addMonoidHom_injective 📖	mathematical	—	AlgHom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring AddMonoidHomClass.toAddMonoidHom funLike DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike RingHom.id MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule SemilinearMapClass.distribMulActionSemiHomClass AlgHomClass.linearMapClass algHomClass	—	RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass RingHom.coe_addMonoidHom_injective coe_ringHom_injective
coe_coe 📖	mathematical	—	DFunLike.coe AlgHom funLike AlgHomClass.toAlgHom	—	—
coe_comp 📖	mathematical	—	DFunLike.coe AlgHom funLike comp	—	—
coe_fn_inj 📖	mathematical	—	DFunLike.coe AlgHom funLike	—	DFunLike.coe_fn_eq
coe_fn_injective 📖	mathematical	—	AlgHom DFunLike.coe funLike	—	DFunLike.coe_injective
coe_id 📖	mathematical	—	DFunLike.coe AlgHom funLike id	—	—
coe_mk 📖	mathematical	OneHom.toFun MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.toOneHom RingHom.toMonoidHom DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	AlgHom funLike	—	—
coe_mk' 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Algebra.toSMul	AlgHom funLike mk'	—	—
coe_mks 📖	mathematical	MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring OneHom.toFun MulOne.toMul MonoidHom.toOneHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddZero.toAdd RingHom.toMonoidHom DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	AlgHom funLike	—	—
coe_monoidHom_injective 📖	mathematical	—	AlgHom MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHomClass.toMonoidHom funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass algHomClass	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.coe_monoidHom_injective coe_ringHom_injective
coe_pow 📖	mathematical	—	DFunLike.coe AlgHom funLike Monoid.toNatPow End Nat.iterate	—	pow_zero pow_succ
coe_ringHom_injective 📖	mathematical	—	AlgHom RingHom Semiring.toNonAssocSemiring RingHomClass.toRingHom funLike AlgHomClass.toRingHomClass algHomClass	—	AlgHomClass.toRingHomClass algHomClass coe_fn_injective
coe_ringHom_mk 📖	mathematical	OneHom.toFun MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.toOneHom RingHom.toMonoidHom DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	RingHomClass.toRingHom AlgHom funLike AlgHomClass.toRingHomClass algHomClass	—	AlgHomClass.toRingHomClass algHomClass
coe_toAddMonoidHom 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring AddMonoidHom.instFunLike AddMonoidHomClass.toAddMonoidHom AlgHom funLike DistribMulActionSemiHomClass.toAddMonoidHomClass RingHom CommSemiring.toSemiring RingHom.instFunLike RingHom.id MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule SemilinearMapClass.distribMulActionSemiHomClass AlgHomClass.linearMapClass algHomClass	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass AlgHomClass.linearMapClass algHomClass
coe_toLinearMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike toLinearMap AlgHom funLike	—	—
coe_toMonoidHom 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.instFunLike MonoidHomClass.toMonoidHom AlgHom funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass algHomClass	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass algHomClass
coe_toRingHom 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHomClass.toRingHom AlgHom funLike AlgHomClass.toRingHomClass algHomClass	—	AlgHomClass.toRingHomClass algHomClass
commutes 📖	mathematical	—	DFunLike.coe AlgHom funLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	commutes'
commutes' 📖	mathematical	—	OneHom.toFun MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.toOneHom RingHom.toMonoidHom toRingHom DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
comp_algebraMap 📖	mathematical	—	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHomClass.toRingHom AlgHom funLike AlgHomClass.toRingHomClass algHomClass algebraMap	—	RingHom.ext AlgHomClass.toRingHomClass algHomClass commutes
comp_apply 📖	mathematical	—	DFunLike.coe AlgHom funLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	—
comp_toLinearMap 📖	mathematical	—	toLinearMap comp LinearMap.comp CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule RingHom.id RingHomCompTriple.ids	—	—
comp_toRingHom 📖	mathematical	—	RingHomClass.toRingHom AlgHom funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass algHomClass comp RingHom.comp	—	AlgHomClass.toRingHomClass algHomClass
congr_arg 📖	mathematical	—	DFunLike.coe AlgHom funLike	—	DFunLike.congr_arg
congr_fun 📖	mathematical	—	DFunLike.coe AlgHom funLike	—	DFunLike.congr_fun
default_apply 📖	mathematical	—	DFunLike.coe AlgHom funLike Unique.instInhabited uniqueOfRight MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
ext 📖	—	DFunLike.coe AlgHom funLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe AlgHom funLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe AlgHom funLike id	—	—
id_comp 📖	mathematical	—	comp id	—	—
id_toRingHom 📖	mathematical	—	RingHomClass.toRingHom AlgHom funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass algHomClass id RingHom.id	—	AlgHomClass.toRingHomClass algHomClass
instRingHomCompTripleComp 📖	mathematical	—	RingHomCompTriple toRingHom comp	—	—
linearMapMk_toAddHom 📖	mathematical	—	CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule AddHomClass.toAddHom AlgHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup funLike SemilinearMapClass.toAddHomClass AlgHomClass.linearMapClass algHomClass map_smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.toMulActionSemiHomClass toLinearMap	—	SemilinearMapClass.toAddHomClass AlgHomClass.linearMapClass algHomClass map_smul SemilinearMapClass.toMulActionSemiHomClass
map_smul_of_tower 📖	mathematical	—	DFunLike.coe AlgHom funLike	—	LinearMap.map_smul_of_tower
mk_coe 📖	—	DFunLike.coe AlgHom funLike MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring OneHom.toFun MulOne.toMul MonoidHom.toOneHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddZero.toAdd RingHom.toMonoidHom RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—	—
mul_apply 📖	mathematical	—	DFunLike.coe AlgHom funLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass End	—	—
ofLinearMap_apply 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	AlgHom funLike ofLinearMap	—	—
ofLinearMap_id 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike LinearMap.id AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	ofLinearMap id	—	—
ofLinearMap_toLinearMap 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike toLinearMap AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	ofLinearMap	—	—
one_apply 📖	mathematical	—	DFunLike.coe AlgHom funLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass End	—	—
toEnd_apply 📖	mathematical	—	DFunLike.coe MonoidHom AlgHom Module.End CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule MulOneClass.toMulOne Monoid.toMulOneClass End MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike toEnd toLinearMap	—	—
toFun_eq_coe 📖	mathematical	—	OneHom.toFun MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.toOneHom RingHom.toMonoidHom toRingHom DFunLike.coe AlgHom funLike	—	—
toLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike toLinearMap AlgHom funLike	—	—
toLinearMap_id 📖	mathematical	—	toLinearMap id LinearMap.id CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule	—	—
toLinearMap_injective 📖	mathematical	—	AlgHom LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule toLinearMap	—	ext LinearMap.congr_fun
toLinearMap_ofLinearMap 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	toLinearMap ofLinearMap	—	—
toRingHom_eq_coe 📖	mathematical	—	toRingHom RingHomClass.toRingHom AlgHom funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass algHomClass	—	—
toRingHom_toAddMonoidHom 📖	mathematical	—	AddMonoidHomClass.toAddMonoidHom RingHom Semiring.toNonAssocSemiring AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne RingHom.instFunLike RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass RingHomClass.toRingHom AlgHom funLike AlgHomClass.toRingHomClass algHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe CommSemiring.toSemiring RingHom.id MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule SemilinearMapClass.distribMulActionSemiHomClass AlgHomClass.linearMapClass	—	RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass algHomClass
toRingHom_toMonoidHom 📖	mathematical	—	MonoidHomClass.toMonoidHom RingHom Semiring.toNonAssocSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHomClass.toRingHom AlgHom funLike AlgHomClass.toRingHomClass algHomClass	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass algHomClass

AlgHom.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—

AlgHomClass

Definitions

Name	Category	Theorems
coeTC 📖	CompOp	—
toAlgHom 📖	CompOp	106 math math: Ideal.quotientEquivAlgOfEq_coe_eq_factorₐ, Subalgebra.mulMap_comm, ContinuousAlgHom.coe_fst, AlgEquiv.toAlgHom_toRingHom, StarAlgEquiv.ofInjective_symm_apply, ContinuousAlgHom.toAlgHomMonoidHom_apply, FractionalIdeal.mapEquiv_apply, MvPolynomial.comapEquiv_symm_coe, Polynomial.toAlgHom_taylorEquiv, Complex.real_algHom_eq_id_or_conj, FractionalIdeal.map_one_div, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, Bialgebra.TensorProduct.map_toAlgHom, Algebra.TensorProduct.congr_symm_apply, ContinuousAlgHom.coe_id, ContinuousAlgHom.coe_eq_id, toRingHom_toAlgHom, MvPolynomial.comapEquiv_coe, AlgHom.coe_coe, integralClosure_map_algEquiv, AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, AlgEquiv.toAlgHom_eq_coe, coe_galRestrict_apply, Polynomial.toMvPolynomial_eq_rename_comp, CommAlgCat.isoMk_hom, BialgHom.coe_toAlgHom, ContinuousAlgHom.coe_codRestrict, BialgHom.coe_algHom_injective, Complex.liftAux_neg_I, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, AddMonoidAlgebra.mapRangeAlgEquiv_apply, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ, AlgEquiv.toAlgHom_toLinearMap, galLiftEquiv_apply, BialgHom.toAlgHom_toLinearMap, BialgCat.forget₂_algebra_map, MonoidAlgebra.mapRangeAlgEquiv_apply, Algebra.TensorProduct.congr_apply, ContinuousAlgHom.coe_restrictScalars, instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom, DenseRange.topologicalClosure_map_subalgebra, ContinuousAlgHom.coe_prod, IntermediateField.normal_iff_forall_map_le', BialgHomClass.counitAlgHom_comp, AlgEquiv.symm_comp, galLiftEquiv_symm_apply, AlgEquiv.toAlgHom_ofBijective, FractionalIdeal.coeFun_mapEquiv, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ, IsAzumaya.coe_tensorEquivEnd, AlgEquiv.coe_algHom_injective, Algebra.TensorProduct.comm_comp_includeRight, Algebra.TensorProduct.comm_comp_includeLeft, AlgEquiv.val_algHomUnitsEquiv_symm_apply, AlgEquiv.refl_toAlgHom, FractionalIdeal.map_div, ContinuousAlgHom.coe_prodMap, FractionalIdeal.map_inv, Polynomial.mapAlgEquiv_toAlgHom, AlgEquiv.toAlgebraIso_inv, Submodule.range_valA, ContinuousAlgHom.coe_inj, AlgEquiv.subalgebraMap_apply_coe, BialgEquiv.toBialgHom_toAlgHom, galRestrict_apply, toLinearMap_toAlgHom, BialgHomClass.map_comp_comulAlgHom, IntermediateField.normalClosure_def'', Subalgebra.map_topologicalClosure_le, IntermediateField.normal_iff_forall_map_eq', minpoly.equivAdjoin_toAlgHom, AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply, AlgEquiv.fieldRange_eq_top, AlgEquiv.comp_symm, ContinuousAlgHom.coe_rangeRestrict, Polynomial.aeval_algEquiv, IsGalois.map_fixingSubgroup, CommAlgCat.isoMk_inv, ContinuousAlgEquiv.comp_coe, ContinuousAlgHom.coe_comp, ContinuousAlgHom.coe_coe, AlgEquiv.coe_algHom_ofAlgHom, Algebra.TensorProduct.comm_comp_map, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, FractionalIdeal.map_map_symm, DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ, IsAdjoinRoot.algEquiv_map, algebraicClosure.map_eq_of_algEquiv, CommBialgCat.forget₂_commAlgCat_map, FractionalIdeal.map_symm_map, StandardEtalePresentation.toPresentation_relation, separableClosure.map_eq_of_algEquiv, BialgHom.comp_toAlgHom, AlgEquiv.subalgebraMap_symm_apply_coe, IsSymmetricAlgebra.equiv_toAlgHom, CommBialgCat.hom_id, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, BialgHom.id_toAlgHom, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, ContinuousAlgHom.toAlgHom_eq_coe, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, ContinuousAlgHom.coe_mk, ContinuousAlgHom.coe_snd, AlgEquiv.coe_ringHom_commutes, AlgEquiv.toAlgebraIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commutes 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
linearMapClass 📖	mathematical	—	LinearMapClass CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule	—	AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass toRingHomClass Algebra.smul_def map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass commutes
toLinearMap_toAlgHom 📖	mathematical	—	SemilinearMapClass.semilinearMap AlgHom CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule RingHom.id toAlgHom AlgHom.funLike linearMapClass AlgHom.algHomClass	—	linearMapClass AlgHom.algHomClass
toRingHomClass 📖	mathematical	—	RingHomClass Semiring.toNonAssocSemiring	—	—
toRingHom_toAlgHom 📖	mathematical	—	RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring toRingHomClass AlgHom.algHomClass toAlgHom	—	toRingHomClass AlgHom.algHomClass

Algebra

Definitions

Name	Category	Theorems
algHom 📖	CompOp	2 math math: Localization.algHom_ext_iff, TensorProduct.includeRight_lid
instMulDistribMulActionAlgHomUnits 📖	CompOp	1 math math: smul_units_def
ofId 📖	CompOp	42 math math: range_ofId, Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_right, MvPolynomial.universalFactorizationMap_comp_map, LinearEquiv.algEquivOfRing_apply, MvPolynomial.aevalTower_ofId, Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, ofId_self, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, comp_ofId, Polynomial.Monic.quotient_isIntegral, Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐ, toRingHom_ofId, Ideal.Fiber.lift_residueField_surjective, MvPolynomial.expand_zero, MonoidAlgebra.scalarTensorEquiv_tmul, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, Polynomial.aevalTower_ofId, AdjoinRoot.Minpoly.coe_toAdjoin, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, MvPolynomial.sumAlgEquiv_comp_rename_inl, exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂, AdjoinRoot.liftAlgHom_eq_algHom, AdjoinRoot.equiv'_toAlgHom, Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_left, ofId_apply, exists_etale_isIdempotentElem_forall_liesOver_eq, TrivSqZeroExt.liftEquivOfComm_apply, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, CommAlgCat.toUnit_unop_hom, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime, PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable, exists_etale_isIdempotentElem_forall_liesOver_eq_aux, AdjoinRoot.equiv'_apply, IsLocalization.map_linearMap_eq_toLinearMap_mapₐ, Pi.constAlgHom_eq_algebra_ofId, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, AddMonoidAlgebra.scalarTensorEquiv_tmul, AdjoinRoot.coe_algHomOfDvd, AdjoinRoot.liftHom_mk, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, WeierstrassCurve.Affine.Point.map_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMapSubmonoid_le_comap 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder algebraMapSubmonoid Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHom.toRingHom	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass algebraMapSubmonoid_map_eq Submonoid.le_comap_map
algebraMapSubmonoid_map_eq 📖	mathematical	—	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring AlgHom AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass algebraMapSubmonoid	—	Submonoid.ext MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.commutes
comp_ofId 📖	mathematical	—	AlgHom.comp CommSemiring.toSemiring id ofId	—	ext_id
ext_id 📖	—	—	—	—	subsingleton_id
ext_id_iff 📖	—	—	—	—	ext_id
ofId_apply 📖	mathematical	—	DFunLike.coe AlgHom CommSemiring.toSemiring id AlgHom.funLike ofId RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	—
ofId_self 📖	mathematical	—	ofId CommSemiring.toSemiring id AlgHom.id	—	—
smul_units_def 📖	mathematical	—	AlgHom Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero SemigroupAction.toSMul Monoid.toSemigroup AlgHom.End MulAction.toSemigroupAction MulDistribMulAction.toMulAction Units.instMonoid instMulDistribMulActionAlgHomUnits DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map MonoidHomClass.toMonoidHom MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass	—	—
subsingleton_id 📖	mathematical	—	AlgHom CommSemiring.toSemiring id	—	AlgHom.ext AlgHom.commutes
toRingHom_ofId 📖	mathematical	—	RingHomClass.toRingHom AlgHom CommSemiring.toSemiring id AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass ofId algebraMap	—	AlgHomClass.toRingHomClass AlgHom.algHomClass

MulSemiringAction

Definitions

Name	Category	Theorems
toAlgHom 📖	CompOp	3 math math: FixedPoints.toAlgHom_bijective, toAlgHom_apply, toAlgHom_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom AlgHom.funLike toAlgHom SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul toDistribMulAction	—	—
toAlgHom_injective 📖	mathematical	—	AlgHom toAlgHom	—	FaithfulSMul.eq_of_smul_eq_smul AlgHom.ext_iff

RingHom

Definitions

Name	Category	Theorems
toIntAlgHom 📖	CompOp	4 math math: toIntAlgHom_apply, CommRingCat.coproductCoconeIsColimit_desc, toIntAlgHom_coe, toIntAlgHom_injective
toNatAlgHom 📖	CompOp	2 math math: toNatAlgHom_coe, toNatAlgHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIntAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom Int.instCommSemiring Ring.toSemiring Ring.toIntAlgebra AlgHom.funLike toIntAlgHom RingHom Semiring.toNonAssocSemiring instFunLike	—	—
toIntAlgHom_coe 📖	mathematical	—	DFunLike.coe AlgHom Int.instCommSemiring Ring.toSemiring Ring.toIntAlgebra AlgHom.funLike toIntAlgHom RingHom Semiring.toNonAssocSemiring instFunLike	—	—
toIntAlgHom_injective 📖	mathematical	—	RingHom Semiring.toNonAssocSemiring Ring.toSemiring AlgHom Int.instCommSemiring Ring.toIntAlgebra toIntAlgHom	—	DFunLike.ext DFunLike.congr_fun
toNatAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom Nat.instCommSemiring Semiring.toNatAlgebra AlgHom.funLike toNatAlgHom RingHom Semiring.toNonAssocSemiring instFunLike	—	—
toNatAlgHom_coe 📖	mathematical	—	DFunLike.coe AlgHom Nat.instCommSemiring Semiring.toNatAlgebra AlgHom.funLike toNatAlgHom RingHom Semiring.toNonAssocSemiring instFunLike	—	—

(root)

Definitions

Name	Category	Theorems
AlgHom 📖	CompData	1770 math math: CommRingCat.tensorProd_map_right, CliffordAlgebra.unop_reverseOp, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, MvPolynomial.join₁_rename, IsSymmetricAlgebra.lift_eq, 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, 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', CommAlgCat.comp_apply, Field.Emb.Cardinal.equivLim_coherence, SymmetricAlgebra.lift_ι_apply, AddMonoidAlgebra.lift_apply', MvPolynomial.algHom_ext_iff, MvPolynomial.map_bind₁, CliffordAlgebra.involute_eq_of_mem_odd, Algebra.Generators.aeval_val_surjective, 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, 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, PowerBasis.exists_eq_aeval, Polynomial.algebraMap_pi_eq_aeval, 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, Polynomial.disjoint_ker_aeval_of_isCoprime, MvPolynomial.universalFactorizationMap_comp_map, MvPolynomial.aeval_algebraMap_eq_zero_iff, MvPowerSeries.support_expand, PolynomialModule.smul_def, FiniteField.nonempty_algHom_of_finrank_dvd, IsAdjoinRoot.mem_ker_map, AlgHom.ker_coe, PowerSeries.coeff_expand_mul, 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, 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, AddMonoidAlgebra.mapRangeAlgHom_single, TensorProduct.toIntegralClosure_bijective_of_isLocalization, Polynomial.mem_rootSet_of_injective, Algebra.TensorProduct.mapOfCompatibleSMul_surjective, Polynomial.aeval_map_algebraMap, TensorAlgebra.toTrivSqZeroExt_ι, MonoidAlgebra.algHom_ext'_iff, eval₂_minpolyDiv_of_eval₂_eq_zero, 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, AlgHom.algHomClass, MvPolynomial.algHom_ext'_iff, IntermediateField.mem_adjoin_iff, RatFunc.laurent_algebraMap, AlgebraicIndependent.repr_ker, AlgHom.IsArithFrobAt.mk_apply, DoubleQuot.coe_quotLeftToQuotSupₐ, MvPolynomial.aeval_X, IntermediateField.algHomEquivAlgHomOfSplits_apply, Rep.to_Module_monoidAlgebra_map_aux, Field.finSepDegree_eq_of_isAlgClosed, 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, MvPolynomial.optionEquivLeft_apply, 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, isConjRoot_algHom_iff, AlgHom.coe_coe, RatFunc.laurent_div, CliffordAlgebraQuaternion.toQuaternion_ofQuaternion, 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, WeierstrassCurve.Projective.baseChange_negY, UniversalEnvelopingAlgebra.lift_unique, RingQuot.mkAlgHom_surjective, DoubleQuot.quotQuotEquivComm_symmₐ, Ideal.Quotient.coe_factorₐ, Polynomial.aeval_iterate_derivative_self, MvPolynomial.aeval_eq_eval, PowerSeries.coeff_heval, Module.endTensorEndAlgHom_apply, MvPolynomial.aeval_ite_mem_eq_self, CliffordAlgebra.toProd_ι_tmul_one, AlgHom.coe_fn_inj, RingCon.quotientKerEquivRangeₐ_comp_mkₐ, Polynomial.mapAlgHom_eq_eval₂AlgHom'_CAlgHom, 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, Finite.algHom, MvPolynomial.eval_rename_prod_mk, AdjoinRoot.algHom_ext_iff, PowerBasis.equivAdjoinSimple_symm_aeval, TrivSqZeroExt.map_inr, MvPolynomial.aevalTower_comp_C, Polynomial.toAddCircle_X_pow_eq_fourier, Subalgebra.val_apply, MvPolynomial.rename_msymm, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd, AlgHom.coe_range, RingHom.toRatAlgHom_apply, IsAlgebraic.algHom, finrank_algHom, MvPolynomial.eval₂Hom_C_eq_bind₁, gelfandTransform_bijective, AlgHom.coe_id, Polynomial.differentiableOn_aeval, 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, 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, IsFractionRing.algHom_commutes, CommAlgCat.ofHom_apply, DualNumber.lift_apply_eps, AdjoinRoot.Minpoly.toAdjoin.surjective, Algebra.TensorProduct.includeRight_apply, Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat, Polynomial.aeval_X_pow, AlgHom.extendScalarsOfSurjective_apply, Polynomial.Bivariate.aveal_eq_map_swap, WeierstrassCurve.baseChange_Ψ₂Sq, IsLocalizedModule.map_linearMap_of_isLocalization, 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, 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.aeval_eq_zero_of_mem_rootSet, Unitization.lift_symm_apply_apply, MvPolynomial.coeff_expand_smul, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, Algebra.Generators.algebraMap_apply, RingHom.toIntAlgHom_apply, 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, 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, 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, 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', NonUnitalSubsemiring.unitization_apply, PowerBasis.leftMulMatrix, MonoidAlgebra.toRingHom_mapRangeAlgHom, CategoryTheory.Iso.toAlgEquiv_symm_apply, linearIndependent_algHom_toLinearMap', MvPolynomial.support_rename_of_injective, MonoidAlgebra.scalarTensorEquiv_tmul, MvPolynomial.ACounit_C, Polynomial.expand_C, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, CommAlgCat.algEquivOfIso_symm_apply, Polynomial.aevalTower_toAlgHom, AlgHom.comp_apply, IsAdjoinRootMonic.map_modByMonic, 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, TensorAlgebra.lift_symm_apply, AddMonoidAlgebra.tensorEquiv.invFun_tmul, PowerSeries.expand_one_apply, 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, AlgHom.prodEquiv_symm_apply, TensorAlgebra.equivDirectSum_apply, Algebra.Presentation.comp_aeval_relation_inl, AdjoinRoot.aeval_eq_of_algebra, RatFunc.laurent_at_zero, WittVector.mulN_coeff, Matrix.isRepresentation.toEnd_represents, DualNumber.lift_inlAlgHom_eps, 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, 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, AlgHom.coe_toMonoidHom, ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf, IntermediateField.adjoin_map, CommAlgCat.lift_unop_hom, RingCon.kerLiftₐ_mk, AlgHom.map_adjugate, map_mem_separableClosure_iff, MvPolynomial.aeval_expand, 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, 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, AlgHom.opComm_apply_apply, CliffordAlgebraComplex.ofComplex_I, AlgHom.IsArithFrobAt.localize_algebraMap, AlgHom.ker_rangeRestrict, AlgEquiv.ofAlgHom_symm_apply, Subalgebra.mvPolynomial_aeval_coe, 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, LocallyConstant.constₐ_apply_apply, PowerBasis.equivAdjoinSimple_aeval, 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, Algebra.FiniteType.iff_quotient_mvPolynomial', Algebra.TensorProduct.includeRight_injective, spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots, TensorAlgebra.lift_comp_ι, StarAlgHom.coe_toAlgHom, CliffordAlgebraQuaternion.equiv_symm_apply, AlgHom.map_det, WeierstrassCurve.Jacobian.baseChange_dblX, AlgHom.mulLeftRight_apply, WeierstrassCurve.Jacobian.baseChange_negDblY, 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.exists_fin_rename, AlgHom.mem_range, galLiftEquiv_apply, AdicCompletion.factorₐ_evalₐ_one, AlgHom.comp_algebraMap_of_tower, Algebra.FiniteType.iff_quotient_freeAlgebra, Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits_apply_apply, AlgHom.mapMatrix_apply, transcendental_aeval_iff, Polynomial.Splits.aeval_eq_prod_aroots, MonoidAlgebra.lift_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, 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, Polynomial.expand_expand, Subalgebra.mulMap'_surjective, Polynomial.mapAlgHom_monomial, AlgHom.IsArithFrobAt.restrict_injective, WittVector.bind₁_wittMulN_wittPolynomial, BialgCat.forget₂_algebra_map, DoubleQuot.coe_quotQuotEquivQuotSupₐ, AnalyticWithinAt.aeval_polynomial, Subalgebra.mem_map, sum_embeddings_eq_finrank_mul, MvPolynomial.aevalTower_C, DirectSum.coeAlgHom_of, MvPolynomial.expand_one_apply, Complex.liftAux_apply_I, MvPolynomial.map_expand_pow_char, MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure, Polynomial.aeval_apply_smul_mem_of_le_comap, 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, Matrix.isRepresentation.toEnd_exists_mem_ideal, Representation.asAlgebraHom_single_one, Algebra.Generators.Hom.toAlgHom_X, MvPolynomial.bind₁_rename, 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, 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, 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, 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, Algebra.TensorProduct.includeRight_bijective, UniversalEnvelopingAlgebra.lift_ι_apply, Algebra.Generators.H1Cotangent.δAux_ofComp, QuaternionAlgebra.lift_symm_apply, TrivSqZeroExt.inlAlgHom_apply, Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, AlgHom.one_apply, PiTensorProduct.singleAlgHom_apply, Polynomial.int_eval₂_eq, AdjoinRoot.liftAlgHom_eq_algHom, 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, 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, AlgHom.card_of_powerBasis, AddMonoidAlgebra.lift_symm_apply, StandardEtalePresentation.toSubmersivePresentation_jacobian, IsAlgClosed.exists_aeval_eq_zero_of_injective, Algebra.IsAlgebraic.algHom_bijective₂, wittStructureInt_prop, Polynomial.expand_eq_zero, Polynomial.differentiableAt_aeval, WeakDual.CharacterSpace.compContinuousMap_apply, Submodule.coe_mulMap_comp_eq, 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, Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splits, AlgHom.compLeft_apply, 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ₐ, Algebra.smulTower_leftMulMatrix, CliffordAlgebra.lift_symm_apply, MvPowerSeries.expand_subst, Module.Finite.exists_free_surjective, galRestrictHom_symm_algebraMap_apply, MvPolynomial.universalFactorizationMapPresentation_relation, AnalyticAt.aeval_polynomial, MvPolynomial.aevalTower_comp_algebraMap, 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, Polynomial.expand_zero, CliffordAlgebraQuaternion.ofQuaternion_mk, WeierstrassCurve.Projective.baseChange_dblZ, Polynomial.roots_expand_pow_map_iterateFrobenius_le, PowerBasis.equivOfMinpoly_aeval, Algebra.Generators.aeval_val_σ, Subalgebra.algebraMap_eq, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ, MvPolynomial.mem_zeroLocus_iff, Polynomial.rootMultiplicity_expand, NonUnitalSubalgebra.unitization_apply, AlgHom.tensorEqualizerEquiv_apply, DualNumber.lift_apply_apply, AlgEquiv.coe_algHom_injective, Algebra.ofId_apply, WeierstrassCurve.Affine.baseChange_addPolynomial, AlgEquiv.arrowCongr_comp, Unitization.lift_symm_apply, transcendental_iff_ker_eq_bot, MonoidAlgebra.tensorEquiv_tmul, 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, MvPowerSeries.substAlgHom_coe, 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, IntermediateField.mem_adjoin_range_iff, CommAlgCat.forget₂_algCat_obj, SymmetricAlgebra.lift_comp_ι, 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_ι, WeierstrassCurve.Jacobian.baseChange_neg, Polynomial.hasDerivWithinAt_aeval, 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, Polynomial.toAddCircle_monomial_eq_smul_fourier, CliffordAlgebra.toBaseChange_comp_reverseOp, 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, Algebra.smul_units_def, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ, AlgHom.congr_arg, MvPolynomial.coeToMvPowerSeries.algHom_apply, IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk, AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc, AlgebraicIndependent.liftAlgHom_comp_reprField, AlgCat.forget₂_module_obj, sectionOfRetractionKerToTensor_algebraMap, MvPolynomial.rename_rightInverse, RingCon.mkₐ_apply, LinearMap.aeval_self_charpoly, WeierstrassCurve.Projective.baseChange_add, Polynomial.rootSet_maps_to', AlgHom.coe_ideal_map, AlgHom.coe_restrictScalars', 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, AddMonoidAlgebra.toRingHom_mapRangeAlgHom, 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, 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, UniversalEnvelopingAlgebra.ι_apply, Polynomial.algHom_ext_iff, Polynomial.coeToPowerSeries.algHom_apply, AdicCompletion.evalOneₐ_of, PowerBasis.equivOfMinpoly_apply, CommAlgCat.forget_map, WeierstrassCurve.map_baseChange, AlgHom.eqOn_adjoin_iff, 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, Polynomial.map_expand_pow_char, 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, not_irreducible_expand, AddMonoidAlgebra.lift_of', liftOfDerivationToSquareZero_apply, Derivation.tensorProductTo_mul, AlgHom.fieldRange_eq_top, 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, FreeAlgebra.lift_unique, AlgHom.subalgebraMap_coe_apply, WeierstrassCurve.Jacobian.baseChange_dblXYZ, Polynomial.coeff_zero_eq_aeval_zero, CliffordAlgebra.prodEquiv_apply, AlgHom.card_le, 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, AlgHom.mem_fieldRange, Algebra.Generators.repr_CotangentSpaceMap, MonoidAlgebra.lift_apply, Polynomial.annIdealGenerator_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_ι, Polynomial.Splits.aeval_eq_prod_aroots_of_monic, 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, 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.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, Polynomial.aeval_eq_prod_aroots_sub_of_splits, MvPolynomial.coeff_rTensorAlgHom_monomial_tmul, MvPolynomial.bind₁_bind₁, TensorProduct.toIntegralClosure_injective_of_flat, Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime, AdicCompletion.mk_ofAlgEquiv_symm_eq_evalOneₐ, Algebra.TensorProduct.productMap_right_apply, Module.End.baseChangeHom_apply_apply, MvPolynomial.rename_polynomial_aeval_X, MvPolynomial.coeff_expand_of_not_dvd, Matrix.isRepresentation.toEnd_surjective, 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, 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, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, Polynomial.Chebyshev.aeval_C, Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply, Polynomial.aeval_eq_sum_range, polyEquivTensor_apply, MvPolynomial.exists_finset_rename₂, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply, WeierstrassCurve.Projective.baseChange_dblU, MvPolynomial.eval_toMvPolynomial, AlgCat.forget₂Module_preservesLimits, 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ₐ, 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, MvPolynomial.transcendental_polynomial_aeval_X, AdjoinRoot.algHom_subsingleton, AlgebraicIndependent.aevalEquiv_apply_coe, MvPolynomial.rename_C, 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_ι, AlgHom.bijective, AlgHom.map_coe_real_complex, 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, AlgHom.End_toOne_one, IsAdjoinRoot.algebraMap_apply, BoundedContinuousFunction.coe_toContinuousMapₐ, StandardEtalePair.aeval_X_g_mul_mk_X, MvPolynomial.pderiv_inr_universalFactorizationMap_X, TrivSqZeroExt.fst_map, Transcendental.aeval, MvPowerSeries.constantCoeff_expand, Representation.ofModule_asAlgebraHom_apply_apply, TensorAlgebra.equivDirectSum_symm_apply, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, galRestrictHom_symm_apply, PowerSeries.continuous_aeval, 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.mem_aroots, WeierstrassCurve.Affine.Point.map_some, ZMod.expand_card, 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, LieRinehartAlgebra.Hom.map_smul_apply, PowerBasis.liftEquiv'_apply_coe, MvPolynomial.mapAlgHom_apply, Algebra.Generators.cotangentRestrict_mk, minpoly.coe_equivAdjoin, Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply, CliffordAlgebra.toProd_one_tmul_ι, MvPowerSeries.substAlgHom_monomial, CliffordAlgebra.toBaseChange_involute, 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, Polynomial.exists_separable_of_irreducible, 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, 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, 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, AdicCompletion.evalOneₐ_surjective, 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, 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, Polynomial.coeff_expand_mul', Polynomial.differentiableWithinAt_aeval, Unitization.norm_splitMul_snd_sq, AdjoinRoot.coe_algEquivOfEq, 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, AlgEquiv.arrowCongr_symm, Polynomial.coeff_zero_eq_aeval_zero', MvPolynomial.isSymmetric_rename, CliffordAlgebra.ofEven_ι, CliffordAlgebra.ofBaseChange_tmul_one, Polynomial.roots_expand_pow, MvPolynomial.universalFactorizationMap_freeMonic, AlgHom.map_adjoin_singleton, Subalgebra.toSubring_subtype, 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, AlgHom.toEnd_apply, MvPolynomial.eval₂_rename_prod_mk, 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, 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, IsLocalization.Away.mapₐ_apply, MvPolynomial.esymmAlgEquiv_apply, 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, Polynomial.Monic.expand, MvPolynomial.aeval_zero', MvPolynomial.weightedTotalDegree_rename_of_injective, Polynomial.aeval_iterate_derivative_of_lt, WeierstrassCurve.Projective.baseChange_polynomialZ, PowerSeries.substAlgHom_coe, DualNumber.lift_comp_inlHom, AlgHom.linearMapMk_toAddHom, 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₁, 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, AlgHom.toRingHom_toMonoidHom, AlgEquiv.toAlgHomHom_apply, Complex.ofRealAm_coe, WeierstrassCurve.Affine.baseChange_polynomialY, Algebra.smulTower_leftMulMatrix_algebraMap_eq, lipschitzGroup.involute_act_ι_mem_range_ι, 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, Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits, MvPolynomial.aeval_prod, IsPurelyInseparable.instNonemptyAlgHomOfPerfectField, RatFunc.aeval_X_left_eq_algebraMap, IsLocalization.algHom_subsingleton, Matrix.toMvPolynomial_mul, LinearAlgebra.FreeProduct.lift_comp_ι, Subalgebra.toSubsemiring_subtype, MvPolynomial.exists_restrict_to_vars, wittStructureInt_rename, AlgHom.restrictNormal_commutes, FiniteField.orderOf_frobeniusAlgHom, TrivSqZeroExt.fstHom_apply, Polynomial.mapAlgHom_coe_ringHom, AlgHom.subsingleton, 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, Subalgebra.mulMap_tmul, RingCon.liftₐ_mk, WeierstrassCurve.Jacobian.baseChange_negY, BialgCat.forget₂_algebra_obj, Polynomial.aeval_natCast, 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, IsSymmetricAlgebra.equiv_toAlgHom, FiniteField.coe_frobeniusAlgHom, Algebra.IsAlgebraic.bijective_of_isScalarTower, WeierstrassCurve.Projective.baseChange_dblY, MonoidAlgebra.mapDomainAlgHom_apply, Pi.evalAlgHom_apply, TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι, AlgebraicGeometry.pullbackSpecIso_hom_snd, IntermediateField.normalClosure_def', Subalgebra.map_toSubsemiring, spectrum.map_polynomial_aeval, IsAlgClosed.surjective_restrictDomain_of_isAlgebraic, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, spinGroup.involute_eq, DoubleQuot.quotLeftToQuotSupₐ_toRingHom, Algebra.Extension.Cotangent.map_mk, MatrixEquivTensor.toFunAlgHom_apply, PowerSeries.heval_mul, Polynomial.toAddCircle_C_eq_smul_fourier_zero, 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, MvPolynomial.aeval_natDegree_le, 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, AlgHom.op_symm_apply_apply, AlgHom.toLieHom_apply, DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv, WittVector.coeff_frobenius, Matrix.aeval_eq_aeval_mod_charpoly, RingCon.quotientQuotientEquivQuotientₐ_coe_coe, 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, 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, Ideal.map_includeLeft_eq, Polynomial.aeval_add, Polynomial.continuousOn_aeval, CliffordAlgebra.equivOfIsometry_apply, MvPowerSeries.substAlgHom_comp_substAlgHom, Polynomial.aeval_sub, 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, 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, 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, AddMonoidAlgebra.mapRangeAlgHom_apply, 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, 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, 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, CommRingCat.Under.equalizer_comp, AlgHom.coe_pow, IsScalarTower.toAlgHom_apply, Polynomial.map_iterateFrobenius_expand, retractionOfSectionOfKerSqZero_tmul_D, MvPolynomial.rename_surjective, AlgCat.instIsRightAdjointForgetAlgHomCarrier, Polynomial.eval₂_algebraMap_X, 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, 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, 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
AlgHomClass 📖	CompData	6 math math: AlgHom.algHomClass, AlgEquivClass.toAlgHomClass, BialgHomClass.toAlgHomClass, StarAlgHom.instAlgHomClass, WeakDual.CharacterSpace.instAlgHomClass, ContinuousAlgHom.instAlgHomClass
uniqueOfRight 📖	CompOp	1 math math: AlgHom.default_apply
«term_→ₐ[_]_» 📖	CompOp	—
«term_→ₐ_» 📖	CompOp	—

---

← Back to Index