Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-02 08:53 2fdc1510

View on Github →

refactor(power_series/basic): generalize order to semirings (#11765) There are still some TODOs about generalizing statements downstream of this file.

Estimated changes

Modified src/data/finset/nat_antidiagonal.lean

added theorem finset.nat.filter_fst_eq_antidiagonal

added theorem finset.nat.filter_snd_eq_antidiagonal

Modified src/ring_theory/power_series/basic.lean

added theorem power_series.X_pow_order_dvd

modified theorem power_series.coeff_of_lt_order

modified theorem power_series.coeff_order

added theorem power_series.exists_coeff_ne_zero_iff_ne_zero

modified def power_series.order

added theorem power_series.order_eq_multiplicity_X

added theorem power_series.order_finite_iff_ne_zero

deleted theorem power_series.order_finite_of_coeff_ne_zero

modified theorem power_series.order_le

modified theorem power_series.order_zero