← all areas

Namespace PowerSeries 44 theorems

• Frobenius twists satisfy the weight-k Hecke congruence mod p PowerSeries.coeff_heckeT_pow_sub_mem_span 2 below · cited by 1 · depth 12
• A p-adic Weierstrass divisibility criterion via Taylor shifts PowerSeries.dvd_of_forall_taylorShift_order_le 0 below · cited by 2 · depth 14
• Truncated Hensel uniqueness for a simple root over K[[X]] PowerSeries.coeff_eq_coeff_of_forall_coeff_eval_eq_zero 12 below · cited by 2 · depth 15
• Integrality plus a denominator forces descent of power series PowerSeries.mem_range_map_of_monic_of_mul_mem_range 0 below · cited by 1 · depth 15
• Divisibility of a from low coefficients of u(X-a)ⁿ-Xⁿ PowerSeries.mem_span_of_coeff_mul_X_sub_C_pow_sub_X_pow_mem_span 0 below · cited by 2 · depth 15
• Evaluation of power series in an adically complete ring PowerSeries.existsUnique_ringHom_of_isAdicComplete 0 below · cited by 2 · depth 16
• Reduction of a saturated lattice of integral power series PowerSeries.exists_eq_C_mul_map_of_mem_span_of_saturated 0 below · cited by 4 · depth 16
• Eisenstein: algebraic power series have geometrically bounded coefficients PowerSeries.exists_norm_coeff_le_mul_pow_of_isAlgebraic_complex 0 below · cited by 1 · depth 16
• O[[X]]/(X-varpi) is a complete discrete valuation ring PowerSeries.isAdicComplete_quotient_span_X_sub_C_of_irreducible 1 below · cited by 11 · depth 16
• Dividing by a unit-led power series keeps coefficients in a subring PowerSeries.coeff_mem_subring_of_coeff_mul_mem 0 below · cited by 1 · depth 17
• Primitive integral representatives over a valuation ring PowerSeries.exists_eq_C_mul_map_and_mem_span_of_mem_span_of_saturated 0 below · cited by 1 · depth 17
• Weierstrass zero count in the open unit disc PowerSeries.exists_finset_sum_order_taylorShift_eq_order_map_residue 0 below · cited by 1 · depth 17
• W[[X]]/(X-varpi^e) is a discrete valuation ring PowerSeries.quotient_span_X_sub_C_pow_of_irreducible 0 below · cited by 16 · depth 17
• Galois descent for E-subspaces of power series PowerSeries.exists_map_eq_sum_smul_map_of_forall_map_algEquiv_mem 0 below · cited by 1 · depth 18
• Completion of a DVR as O[[X]]/(X-varpi) PowerSeries.exists_ringEquiv_adicCompletion_quotient_span_X_sub_C 2 below · cited by 3 · depth 18
• Descent of coefficients in K₀-linear combinations of power series PowerSeries.exists_sum_smul_eq_of_forall_coeff_mem 0 below · cited by 3 · depth 18
• Normality of D[[s][X]/(X²-sX+varpi^e) PowerSeries.isIntegrallyClosed_adjoinRoot_X_sq_sub_C_X_mul_X_add_C_C_pow 0 below · cited by 2 · depth 18
• Regularised one-sided Schwarz–Jensen bound on a disc PowerSeries.norm_coeff_mul_pow_le_mul_prod_of_forall_coeff_eq_zero 11 below · cited by 2 · depth 18
• Gauss-norm bound for sums of scaled products of power series PowerSeries.norm_coeff_sum_C_mul_prod_mul_pow_le 1 below · cited by 2 · depth 18
• Primality of X² - sX + c over D[[s]] PowerSeries.prime_X_sq_sub_C_X_mul_X_add_C_C 0 below · cited by 2 · depth 18
• Taylor shift of a sum of scaled products of bounded series PowerSeries.taylorShift_sum_C_mul_prod 9 below · cited by 1 · depth 18
• Constant coefficient of the Taylor shift equals F(a) PowerSeries.coeff_zero_taylorShift 0 below · cited by 3 · depth 19
• Identity principle for bounded power series on a disc PowerSeries.eq_of_forall_tsum_coeff_mul_pow_eq 1 below · cited by 2 · depth 19
• Dividing out a zero of a bounded power series PowerSeries.exists_eq_X_sub_C_mul_of_tsum_eq_zero 0 below · cited by 2 · depth 19
• Submultiplicativity of the bound at radius ρ PowerSeries.norm_coeff_mul_mul_pow_le 0 below · cited by 4 · depth 19
• Taylor shift inside the disc preserves the Gauss bound PowerSeries.norm_coeff_taylorShift_mul_pow_le 0 below · cited by 3 · depth 19
• One-sided Schwarz–Jensen bound over a prescribed multiset of zeros PowerSeries.norm_tsum_coeff_mul_pow_le_mul_prod 10 below · cited by 2 · depth 19
• Convergence and bound on the open disc of radius ρ PowerSeries.summable_and_norm_tsum_coeff_mul_pow_le 0 below · cited by 3 · depth 19
• Taylor shift of X-w at a equals (a-w)+X PowerSeries.taylorShift_X_sub_C 0 below · cited by 2 · depth 19
• Additivity of the Taylor shift of bounded power series PowerSeries.taylorShift_add 1 below · cited by 2 · depth 19
• Multiplicativity of the Taylor shift on a disc PowerSeries.taylorShift_mul 6 below · cited by 4 · depth 19
• Evaluation of power series on a disc is multiplicative PowerSeries.tsum_coeff_mul_mul_pow_eq_of_norm_lt 0 below · cited by 3 · depth 19
• Taylor shift recentres a bounded power series PowerSeries.tsum_coeff_taylorShift_mul_pow_eq 0 below · cited by 2 · depth 19
• Power series with non-unit constant term acquire a root PowerSeries.exists_ringHom_valuationSubring_map_eq_zero_of_constantCoeff_mem_maximalIdeal 0 below · cited by 2 · depth 23
• Divisibility of low coefficients of u(X+d)ⁿ-Xⁿ PowerSeries.dvd_coeff_of_smul_eq_mul_X_add_C_pow_sub_X_pow 0 below · cited by 1 · depth 26
• Integrality of power-series expansions from t-adic digits PowerSeries.exists_map_algebraMap_eq_of_digits 0 below · cited by 1 · depth 29
• Invariants of a finite group acting on W[[X]] form a power-series ring PowerSeries.nonempty_algEquiv_of_forall_mem_iff_forall_apply_eq 0 below · cited by 1 · depth 31
• Krull dimension of R[[X]] for Noetherian local R PowerSeries.ringKrullDim_powerSeries 0 below · cited by 1 · depth 34
• Counting linear factors via reduction to unit· X^N PowerSeries.card_eq_of_isUnit_mul_eq_prod_X_sub_C_of_map_residue_eq_mul_X_pow 0 below · cited by 1 · depth 35
• Equal principal ideals in T[[X]] force a unit multiple PowerSeries.exists_isUnit_mul_eq_prod_X_sub_C_of_span_eq 0 below · cited by 1 · depth 36
• Weierstrass preparation from a factorisation u· X^N over the residue field PowerSeries.exists_monic_natDegree_eq_mul_of_map_eq_mul_X_pow 0 below · cited by 1 · depth 36
• Unique evaluation of power series at a nilpotent element PowerSeries.existsUnique_algHom_apply_X_eq_of_isNilpotent 0 below · cited by 1 · depth 38
• O[[t]] is a complete regular local ring of dimension at most 2 PowerSeries.exists_isRegularLocalRing_isRegularRing_ringKrullDim_le_two_of_isDiscreteValuationRing 7 below · cited by 1 · depth 39
• Reduction tower and τ : O[[X]]/𝔪² → k[ε] PowerSeries.exists_bijective_residue_reduction_dualNumber_of_isDiscreteValuationRing 0 below · cited by 1 · depth 40