Commit 2024-12-01 10:47 90f9e991

View on Github →

chore: remove PartENat from PowerSeries (#19622)

Estimated changes

added theorem ENat.add_lt_top
added theorem ENat.coe_inj
added theorem ENat.coe_le_coe
added theorem ENat.coe_lift
added theorem ENat.coe_lt_coe
added theorem ENat.le_lift_iff
added def ENat.lift
added theorem ENat.lift_add
added theorem ENat.lift_coe
added theorem ENat.lift_le_iff
added theorem ENat.lift_lt_iff
added theorem ENat.lift_ofNat
added theorem ENat.lift_one
added theorem ENat.lift_zero
added theorem ENat.lt_lift_iff
modified theorem PowerSeries.X_pow_order_dvd
modified theorem PowerSeries.coeff_order
modified theorem PowerSeries.le_order
modified def PowerSeries.order
modified theorem PowerSeries.order_eq
modified theorem PowerSeries.order_eq_top