Commit 2024-10-10 07:46 8a434b09

View on Github →

feat(RingTheory/LaurentSeries): add notation (#16639) Refs: leanprover/vscode-lean4#523

Estimated changes

Modified Mathlib/RingTheory/LaurentSeries.lean

modified def LaurentSeries.Cauchy.coeff

modified theorem LaurentSeries.Cauchy.coeff_eventually_equal

modified theorem LaurentSeries.Cauchy.coeff_support_bddBelow

modified theorem LaurentSeries.Cauchy.coeff_tendsto

modified theorem LaurentSeries.Cauchy.eventually_mem_nhds

modified theorem LaurentSeries.Cauchy.exists_lb_coeff_ne

modified theorem LaurentSeries.Cauchy.exists_lb_eventual_support

modified theorem LaurentSeries.Cauchy.exists_lb_support

modified def LaurentSeries.Cauchy.limit

modified theorem LaurentSeries.coeff_coe_powerSeries

modified theorem LaurentSeries.coeff_zero_of_lt_valuation

modified theorem LaurentSeries.eq_coeff_of_valuation_sub_lt

modified theorem LaurentSeries.hasseDeriv_coeff

modified theorem LaurentSeries.ofPowerSeries_powerSeriesPart

modified def LaurentSeries.powerSeriesPart

modified theorem LaurentSeries.powerSeriesPart_coeff

modified theorem LaurentSeries.powerSeriesPart_eq_zero

modified theorem LaurentSeries.powerSeriesPart_zero

modified theorem LaurentSeries.single_order_mul_powerSeriesPart

modified theorem LaurentSeries.val_le_one_iff_eq_coe

modified theorem LaurentSeries.valuation_le_iff_coeff_lt_eq_zero

modified theorem PowerSeries.coe_C

modified theorem PowerSeries.coe_X

modified theorem PowerSeries.coe_add

modified theorem PowerSeries.coe_mul

modified theorem PowerSeries.coe_neg

modified theorem PowerSeries.coe_one

modified theorem PowerSeries.coe_pow

modified theorem PowerSeries.coe_smul

modified theorem PowerSeries.coe_sub

modified theorem PowerSeries.coe_zero

modified def RatFunc.coeAlgHom

modified def RatFunc.coeToLaurentSeries_fun

modified theorem RatFunc.coe_C

modified theorem RatFunc.coe_X

modified theorem RatFunc.coe_add

modified theorem RatFunc.coe_coe

modified theorem RatFunc.coe_def

modified theorem RatFunc.coe_div

modified theorem RatFunc.coe_injective

modified theorem RatFunc.coe_mul

modified theorem RatFunc.coe_ne_zero

modified theorem RatFunc.coe_neg

modified theorem RatFunc.coe_num_denom

modified theorem RatFunc.coe_one

modified theorem RatFunc.coe_pow

modified theorem RatFunc.coe_smul

modified theorem RatFunc.coe_sub

modified theorem RatFunc.coe_zero