Commit 2024-04-17 16:44 85a47191

View on Github →

feat (RingTheory/PowerSeries): Add basic lemmas aiming at proving that power series over a field are a DVR (#12160) Add some basic lemmas about (univariate) power series over fields and their inverses, aiming at proving that they form a DVR.

Estimated changes

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

added theorem PowerSeries.C_injective

added theorem PowerSeries.X_irreducible

added theorem PowerSeries.constantCoeff_surj

added theorem PowerSeries.not_isField

Modified Mathlib/RingTheory/PowerSeries/Inverse.lean

added def PowerSeries.Inv_divided_by_X_pow_order

added theorem PowerSeries.Inv_divided_by_X_pow_order_leftInv

added theorem PowerSeries.Inv_divided_by_X_pow_order_rightInv

added def PowerSeries.Unit_of_divided_by_X_pow_order

added theorem PowerSeries.Unit_of_divided_by_X_pow_order_nonzero

added theorem PowerSeries.Unit_of_divided_by_X_pow_order_zero

modified theorem PowerSeries.X_inv

modified theorem PowerSeries.coeff_inv

modified theorem PowerSeries.constantCoeff_inv

added theorem PowerSeries.eq_divided_by_X_pow_order_Iff_Unit

modified theorem PowerSeries.eq_inv_iff_mul_eq_one

modified theorem PowerSeries.eq_mul_inv_iff_mul_eq

added def PowerSeries.firstUnitCoeff

added theorem PowerSeries.hasUnitMulPowIrreducibleFactorization

modified theorem PowerSeries.invOfUnit_eq'

modified theorem PowerSeries.invOfUnit_eq

modified theorem PowerSeries.inv_eq_iff_mul_eq_one

modified theorem PowerSeries.inv_eq_inv_aux

modified theorem PowerSeries.inv_eq_zero

added theorem PowerSeries.isUnit_divided_by_X_pow_order

added theorem PowerSeries.ker_coeff_eq_max_ideal

added theorem PowerSeries.maximalIdeal_eq_span_X

added def PowerSeries.residueFieldOfPowerSeries

modified theorem PowerSeries.smul_inv

modified theorem PowerSeries.zero_inv

Modified Mathlib/RingTheory/PowerSeries/Order.lean

added def PowerSeries.divided_by_X_pow_order

added theorem PowerSeries.divided_by_X_pow_orderMul

added theorem PowerSeries.divided_by_X_pow_order_of_X_eq_one

added theorem PowerSeries.order_zero_of_unit

added theorem PowerSeries.self_eq_X_pow_order_mul_divided_by_X_pow_order