← all areas

Namespace MvPowerSeries 81 theorems

• Surjectivity criterion for maps from a power series algebra MvPowerSeries.algHom_surjective_of_apply_X_eq 0 below · cited by 4 · depth 9
• Substitution of ideal elements into multivariate power series MvPowerSeries.exists_algHom_apply_X_eq 0 below · cited by 12 · depth 9
• Adic completeness of multivariate power series over a complete local ring MvPowerSeries.isAdicComplete_maximalIdeal 0 below · cited by 20 · depth 9
• Power series in finitely many variables over a Noetherian ring MvPowerSeries.isNoetherianRing_of_finite 0 below · cited by 25 · depth 9
• (varpi, X₁,…,Xₙ) is regular on R[[X₁,…,Xₙ]] MvPowerSeries.isRegular_C_cons_X 0 below · cited by 2 · depth 9
• Power series vanishing below degree k lie in (X)^k MvPowerSeries.mem_pow_span_X_of_coeff_eq_zero 0 below · cited by 29 · depth 9
• The maximal ideal of R[[X₁,…,Xₙ]] is (varpi,X₁,…,Xₙ) MvPowerSeries.ofList_C_cons_X_eq_maximalIdeal 0 below · cited by 2 · depth 9
• Socle of a finite complete intersection is generated by det g MvPowerSeries.quotient_mk_det_mem_of_ne_bot 1 below · cited by 3 · depth 9
• Residue field of R[[X_σ]] comes from R MvPowerSeries.residue_comp_C_surjective 0 below · cited by 1 · depth 9
• Uniqueness of algebra maps from a power series ring MvPowerSeries.algHom_ext_of_apply_X_mem 0 below · cited by 9 · depth 10
• Tate's computation of Ann_T(kerπ) and η_T MvPowerSeries.annihilator_ker_eq_span_det 2 below · cited by 1 · depth 10
• Freeness of 𝒪[[X₁,…,Xᵣ]] over itself along Xᵢ ↦ fᵢ MvPowerSeries.exists_coords_of_quotient_span_finite_free 10 below · cited by 1 · depth 10
• Reducing power series coefficients modulo a finitely generated ideal MvPowerSeries.exists_algEquiv_quotient_map_C 0 below · cited by 1 · depth 11
• Maximal ideal of a multivariate power series ring MvPowerSeries.maximalIdeal_eq_comap_constantCoeff 0 below · cited by 1 · depth 11
• Maximal ideal of a power series ring over a local ring MvPowerSeries.maximalIdeal_eq_map_C_sup_span_X 0 below · cited by 1 · depth 11
• Frobenius pairing on a finite power-series quotient MvPowerSeries.exists_bijective_compr2_mul_of_finite 2 below · cited by 2 · depth 14
• Formal inverse function theorem in two variables MvPowerSeries.exists_algEquiv_apply_X_eq 0 below · cited by 5 · depth 18
• Krull dimension of 𝒪[[X₁,…,Xₙ]] over a discrete valuation ring MvPowerSeries.ringKrullDim_fin_eq_of_isDiscreteValuationRing 0 below · cited by 14 · depth 18
• Every two-variable power series is A + Bu with A,B symmetric MvPowerSeries.exists_rename_swap_eq_add_mul_X 8 below · cited by 2 · depth 19
• Power series in finitely many variables over a Noetherian ring MvPowerSeries.isNoetherianRing_fin 0 below · cited by 7 · depth 21
• First-order term of substitution into a multivariable power series MvPowerSeries.coeff_sumElim_single_subst_add_sum_X_mul_eq 0 below · cited by 6 · depth 22
• Restrictedness of the formal inverse via a polynomial inverse mod p MvPowerSeries.eventually_coeff_mem_span_pow_of_subst_eq_X_of_exists_polynomial_inverse_mod 0 below · cited by 1 · depth 23
• Integral logarithmic covector of a formal-group logarithm MvPowerSeries.exists_wittVector_forall_coeff_ghostComponent_eq_logCovector 2 below · cited by 2 · depth 23
• Power series presentation from special-fibre coordinates MvPowerSeries.exists_algHom_adicEval_forall_comp_eq_of_specialFibre_coordinates 2 below · cited by 1 · depth 24
• f(Xᵖ) ≡ f(X)ᵖ mod p for multivariate power series MvPowerSeries.expand_sub_pow_mem_span_natCast 0 below · cited by 2 · depth 24
• Dwork-type lifting of a power series to ghost components MvPowerSeries.exists_wittVector_forall_coeff_ghostComponent_eq_of_forall_natCast_mul_coeff_mem 2 below · cited by 3 · depth 25
• Degree bound for Witt components via the Dwork recursion MvPowerSeries.le_mul_degree_of_coeff_coeff_ne_zero_of_forall_coeff_ghostComponent_eq 0 below · cited by 3 · depth 25
• Coefficient of Y⁰ in f(A+YB) equals f(A) MvPowerSeries.coeff_sumElim_zero_subst_add_sum_X_mul_eq 0 below · cited by 3 · depth 26
• Yoneda lemma for formal affine space on nilpotent ideals MvPowerSeries.existsUnique_apply_eq_adicEval_of_natural_of_isNilpotent 0 below · cited by 7 · depth 29
• Division by Xᵢ - bᵢ over a J-adically complete ring MvPowerSeries.exists_C_add_sum_X_sub_C_mul_of_mem_radical_of_isAdicComplete 0 below · cited by 2 · depth 29
• Multiplicativity of dim_k k[[X]]/(f) under substitution MvPowerSeries.finite_and_finrank_quotient_span_range_subst_eq_mul 8 below · cited by 5 · depth 29
• Ideal of the variables equals kernel of constantCoeff MvPowerSeries.span_range_X_eq_ker_constantCoeff 1 below · cited by 25 · depth 29
• Injectivity of substitution along the doubled system (ρ(x),ρ(y)) MvPowerSeries.subst_sumElim_injective_of_finite_projective_quotient_of_X_pow_mem_span 15 below · cited by 3 · depth 29
• Tensor decomposition of S[[xsqcup y]]/(φ(x),φ(y)) MvPowerSeries.exists_algEquiv_quotient_sum_tensorProduct_quotient_apply_mk_rename_mul_rename 1 below · cited by 1 · depth 30
• Expansion of power series along substituted generators MvPowerSeries.exists_eq_sum_subst_mul_of_span_quotient_eq_top 1 below · cited by 4 · depth 30
• Base change of automorphisms of a power-series hypersurface MvPowerSeries.exists_ringEquiv_quotient_span_comp_map_eq_of_ringEquiv_of_linearPart_of_span_eq 1 below · cited by 2 · depth 30
• Finiteness, flatness and freeness of power series substitutions MvPowerSeries.finite_flat_exists_basis_substAlgHom_of_finite_quotient 5 below · cited by 16 · depth 30
• Quotient by cᵢXᵢ+Xᵢ^{Nᵢ}, cᵢ nilpotent, is free of rank prod Nᵢ MvPowerSeries.free_and_finite_and_finrank_quotient_span_range_C_mul_X_add_X_pow_of_isNilpotent 0 below · cited by 1 · depth 30
• Truncated multivariate power series: free of rank prod Nᵢ MvPowerSeries.free_and_finite_and_finrank_quotient_span_range_X_pow 0 below · cited by 6 · depth 30
• Freeness and fibrewise rank of B[[x]]/(ρ) MvPowerSeries.free_quotient_and_finrank_quotient_map_eq_of_finite_of_isLocalRing 12 below · cited by 3 · depth 30
• Coefficientwise criterion for membership in (varpi, X₀,…,X_{k-1}) MvPowerSeries.mem_span_C_sup_ofList_take_iff 0 below · cited by 1 · depth 30
• Injectivity of substitution along ρ with finite quotient MvPowerSeries.subst_injective_of_finite_projective_quotient_of_X_pow_mem_span 12 below · cited by 3 · depth 30
• Depth equals Krull dimension for 𝒪[[X₁,…,Xₙ]] MvPowerSeries.depth_self_eq_ringKrullDim_fin_of_isDiscreteValuationRing 0 below · cited by 1 · depth 31
• Depth of 𝒪[[X₁,…,Xₙ]] over a discrete valuation ring MvPowerSeries.depth_self_fin_eq_of_isDiscreteValuationRing 0 below · cited by 1 · depth 31
• Base change of a power-series quotient with nilpotent variables MvPowerSeries.exists_algEquiv_tensorProduct_quotient_span_map_of_X_pow_mem 0 below · cited by 16 · depth 31
• Base change of power-series quotients by ideals containing (X)^N MvPowerSeries.exists_algEquiv_tensorProduct_quotient_span_map_of_pow_span_X_le 0 below · cited by 2 · depth 31
• Free basis for B[[x]] over substitution by ρ MvPowerSeries.exists_basis_subst_of_finite_quotient_of_isLocalRing 11 below · cited by 3 · depth 31
• Factoring a power series with distinct linear lowest form MvPowerSeries.exists_isUnit_mul_prod_eq_of_sub_prod_linear_mem_pow 5 below · cited by 4 · depth 31
• Powers of (X₀,X₁) in W[[X₀,X₁]] via low-degree coefficients MvPowerSeries.mem_span_X_pow_iff_forall_coeff_eq_zero_of_degree_lt 0 below · cited by 19 · depth 31
• Unique expansions along a lifted residue-field basis MvPowerSeries.existsUnique_eq_sum_subst_mul_of_basis_residueField_tensor_quotient 10 below · cited by 2 · depth 32
• Initial form of g ∈ (X₀,X₁)ᵈ under a ring map MvPowerSeries.exists_apply_eq_mul_pow_mul_add_of_mem_span_X_pow_of_apply_X_eq_mul 0 below · cited by 2 · depth 32
• Splitting off a simple tangent line of a plane power series MvPowerSeries.exists_eq_mul_of_sub_mul_prod_linear_mem_pow_of_det_ne_zero 4 below · cited by 1 · depth 32
• Special fibre of W[[X_σ]]/(g) modulo π MvPowerSeries.exists_ringEquiv_quotient_quotient_span_C_of_maximalIdeal_eq_span 0 below · cited by 4 · depth 32
• Partial q-th power substitution multiplies codimension by q^{d-|T|} MvPowerSeries.finite_and_finrank_quotient_span_range_subst_ite_X_pow_eq 6 below · cited by 1 · depth 32
• Quotients of W[[X₁,…,Xₙ]] are Noetherian and adically complete MvPowerSeries.isNoetherianRing_and_isAdicComplete_map_maximalIdeal_quotient 0 below · cited by 1 · depth 32
• Initial forms multiply: Gh^k lies in (X₀,X₁)^{dk} MvPowerSeries.mul_pow_mem_span_X_pow_and_sum_coeff_mul_pow_eq_constantCoeff_mul_pow 1 below · cited by 2 · depth 32
• Power series with non-zero linear part: prime ideal and tangent line MvPowerSeries.span_singleton_isPrime_of_sub_linear_mem_sq 1 below · cited by 4 · depth 32
• Injectivity of expansion along a substitution over a local ring MvPowerSeries.eq_of_sum_subst_mul_eq_of_basis_quotient_map_residue 6 below · cited by 2 · depth 33
• Factor theorem in R[[X₀,X₁]] for a root X₁=φ(X₀) MvPowerSeries.exists_eq_X_sub_subst_mul_of_subst_eq_zero 1 below · cited by 1 · depth 33
• Finite freeness of A[[X]]/(f₁,…,f_d) over an Artinian local ring MvPowerSeries.finite_free_finrank_quotient_span_eq_of_isArtinianRing_of_finite_map 8 below · cited by 2 · depth 33
• Lifting nilpotence of coordinates along a nilpotent thickening MvPowerSeries.exists_X_pow_mem_span_of_X_pow_mem_span_map_of_surjective_of_isNilpotent 0 below · cited by 1 · depth 34
• Taylor division by X₁-φ(X₀) in two-variable power series MvPowerSeries.exists_eq_X_sub_subst_mul_add_subst_of_constantCoeff_eq_zero 0 below · cited by 2 · depth 34
• Weighted initial form of a multiple is a multiple of the initial form MvPowerSeries.exists_forall_coeff_mul_eq_pow_mul_and_residue_eq_coeff_mul_of_weightedInitialForm_ne_zero 0 below · cited by 1 · depth 34
• Reducedness of the special fibre of a Drinfeld crossing chart MvPowerSeries.isReduced_residueField_tensorProduct_quotient_span_C_mul_sub_mul_of_sub_drinfeldForm_mem_pow 4 below · cited by 2 · depth 35
• Reducedness of k[[X₀,X₁]]/(f) for a Drinfeld-type crossing MvPowerSeries.isReduced_quotient_span_of_sub_drinfeld_mem_pow 2 below · cited by 1 · depth 36
• Finiteness of a power-series quotient killing powers of the variables MvPowerSeries.module_finite_quotient_of_forall_X_pow_mem 0 below · cited by 1 · depth 36
• Scalars annihilating an ideal see power series modulo it MvPowerSeries.smul_eq_smul_of_forall_coeff_sub_mem_of_forall_mul_eq_zero 0 below · cited by 4 · depth 36
• First-order expansion of substitution along a square-zero increment MvPowerSeries.subst_add_sum_smul_eq_add_sum_smul_mul_subst_pderiv 2 below · cited by 7 · depth 36
• Injectivity of substitution along ρ over a local Noetherian base MvPowerSeries.subst_injective_of_finite_quotient_of_X_pow_mem_span_of_isLocalRing 12 below · cited by 1 · depth 36
• Branches of a Drinfeld-type plane curve singularity MvPowerSeries.exists_powerSeries_subst_eq_zero_of_sub_drinfeld_mem_pow 0 below · cited by 1 · depth 37
• Freeness on a basic open chart for power series quotients MvPowerSeries.exists_notMem_and_forall_free_quotient_map_of_projective_of_isMaximal 1 below · cited by 1 · depth 38
• Nakayama: two generators for J after inverting g notin n MvPowerSeries.exists_notMem_and_forall_span_pair_map_eq_map_of_forall_exists_coeff_sub_mem 1 below · cited by 1 · depth 38
• Leibniz rule for `pderivLin` on multivariate power series MvPowerSeries.pderiv_mul 0 below · cited by 2 · depth 38
• Chain rule for formal partial derivatives under substitution MvPowerSeries.pderiv_subst 1 below · cited by 1 · depth 38
• Power series in finitely many variables over a noetherian ring MvPowerSeries.isNoetherianRing_fin_of_isNoetherianRing 0 below · cited by 4 · depth 39
• Vanishing at all truncated points gives membership in I(y) MvPowerSeries.mem_span_image_subst_inr_of_forall_adicEval_eq_zero_of_surjective 1 below · cited by 1 · depth 39
• Descent of ideal membership along an injective substitution MvPowerSeries.mem_span_image_subst_of_subst_mem_span_image_subst_of_projective 1 below · cited by 1 · depth 39
• Splitting one variable off R[[X₀,…,Xₙ]] MvPowerSeries.exists_algEquiv_powerSeries_fin_succ 0 below · cited by 1 · depth 40
• Hazewinkel functional-equation lemma: integrality of Theta MvPowerSeries.exists_map_padicInt_eq_of_subst_log_eq_of_functionalEquation 0 below · cited by 1 · depth 40
• Syzygies of finitely many series in two variables are free MvPowerSeries.exists_basis_ker_linearCombination_of_ne_zero 1 below · cited by 1 · depth 41
• Fibre dimension of a finite power-series quotient under specialisation MvPowerSeries.finrank_quotient_map_eq_of_ker_le 13 below · cited by 2 · depth 43