← all areas

Namespace LaurentSeries 22 theorems

• Order-preserving renormalisation of an embedding into K((X)) LaurentSeries.exists_algHom_comp_map_eq_single 0 below · cited by 1 · depth 12
• K is algebraically closed in K((X)) LaurentSeries.eq_C_coeff_zero_of_isAlgebraic 0 below · cited by 6 · depth 13
• A field is algebraically closed in its Laurent series field LaurentSeries.exists_eq_C_of_isAlgebraic 0 below · cited by 5 · depth 14
• Vanishing coefficients of ℓ-th powers in characteristic ℓ LaurentSeries.coeff_pow_ringChar_eq_zero_of_not_dvd 0 below · cited by 1 · depth 15
• Residue of a logarithmic derivative equals the order LaurentSeries.coeff_neg_one_inv_mul_derivative 1 below · cited by 1 · depth 18
• Residue of ω v in characteristic q with s^q v = 1 LaurentSeries.coeff_neg_one_mul_inv_pow_uniformizer 2 below · cited by 1 · depth 18
• Leibniz rule for the derivative of Laurent series LaurentSeries.derivative_mul 0 below · cited by 3 · depth 18
• Coefficients of the q-th power of a Laurent series in characteristic q LaurentSeries.coeff_pow_char 1 below · cited by 5 · depth 19
• Commuting formal Hecke operators T_ℓ, T_{ℓ'} for coprime ℓ,ℓ' LaurentSeries.commute_heckeT_heckeT 3 below · cited by 1 · depth 19
• Uₚ commutes with T_ℓ for coprime p,ℓ LaurentSeries.commute_heckeU_heckeT 2 below · cited by 1 · depth 19
• Commutativity of Uₐ and U_b on Laurent series LaurentSeries.commute_heckeU_heckeU 0 below · cited by 3 · depth 19
• V_ℓ on Laurent series equals substitution q↦ q^ℓ LaurentSeries.heckeV_eq_qExpand 0 below · cited by 1 · depth 19
• Uₚ and V_ℓ commute on Laurent series for coprime p,ℓ LaurentSeries.commute_heckeU_heckeV 0 below · cited by 2 · depth 20
• V_ℓ and V_{ℓ'} commute on Laurent series LaurentSeries.commute_heckeV_heckeV 0 below · cited by 1 · depth 20
• Hecke eigen-Laurent series with a₁ = 0 vanishes LaurentSeries.eq_zero_of_heckeT_eq_smul_of_heckeU_eq_smul_of_coeff_one_eq_zero 0 below · cited by 1 · depth 20
• Units of Laurent series descend to finitely generated subalgebras LaurentSeries.exists_fg_subalgebra_isUnit_map_of_isUnit_map 0 below · cited by 1 · depth 21
• Separability of finite extensions of k(t) inside k((q)) LaurentSeries.algebraIsSeparable_adjoin_simple_of_forall_pow_ne 0 below · cited by 1 · depth 22
• Echelon basis with integral coefficients and unit pivots LaurentSeries.exists_basis_forall_coeff_mem_valuationSubring_and_coeff_eq_ite 0 below · cited by 1 · depth 25
• Injectivity of K ⊗_k k((q)) → K((q)) LaurentSeries.injective_of_forall_apply_tmul_eq_smul_map 0 below · cited by 3 · depth 29
• Integral Laurent series over i(R)-coefficient subrings have R-coefficients LaurentSeries.exists_forall_coeff_eq_of_isIntegral_of_mem_closure_range_ofPowerSeries 0 below · cited by 1 · depth 30
• Roots of unity in subfields of k₀((X)) are constants in A₀ LaurentSeries.exists_valuationSubring_pow_eq_one_algebraMap_eq_of_pow_eq_one 1 below · cited by 1 · depth 30
• Coefficients of c Z⁻¹ lie in I for unit leading coefficient LaurentSeries.forall_coeff_mem_map_maximalIdeal_of_mul_eq_C_of_forall_coeff_mem_range_of_isUnit_coeff_order 0 below · cited by 2 · depth 36