[Merged by Bors] - feat (RingTheory/PowerSeries/Order) : compute order of power and generalize

[AntoineChambert-Loir]

• compute order of power of power series
• generalize order_mul
• generalize lemmas at the end to [Semiring R] [NoZeroDivisors R] by proving (PowerSeries.X_pow_mul_cancel) that one can divide out by powers on X on both sides
  of an equality.

---

[github-actions]

PR summary a61bad53f5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ X_mul_cancel
+ X_mul_inj
+ X_mul_pow_inj
+ X_pow_mul_cancel
+ commute_X_pow
+ instance [Ring R] [IsDomain R] : IsDomain R⟦X⟧
+ le_order_pow
+ mul_X_cancel
+ mul_X_inj
+ mul_X_pow_cancel
+ mul_X_pow_inj
+ order_pow
+ trichotomy_of_mul_eq_mul
- eq_zero_or_eq_zero_of_mul_eq_zero
- instance [IsDomain R] : IsDomain R⟦X⟧

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[AntoineChambert-Loir]

Since I'm here, I'll also prove that X is not a zero divisor and make the last lemma work for Semiring…

[faenuccio]

LGTM, thanks!

[Ruben-VandeVelde]

Followup: divided_by_X_pow_order should be using camelCase

[Ruben-VandeVelde]

The name suggests the theorem says X = 1 → divided_by_X_pow_order ...something.... Probably you should just drop the of_. Oh, but you're only moving it. Followup, then.

[AntoineChambert-Loir]

Indeed, I was just moving this from one section to another with less assumptions.
Also, @ADedecker is now rewriting part of it, so I'll wait a little bit for that.

[ADedecker]

@Ruben-VandeVelde you might be interested in #24072 which does a preliminary cleanup of these files.

[riccardobrasca]

@Ruben-VandeVelde you might be interested in #24072 which does a preliminary cleanup of these files.

Which one should be reviewed first? Or they're independent?

[AntoineChambert-Loir]

We don't mind. We can coordinate.

[ADedecker]

@Ruben-VandeVelde you might be interested in #24072 which does a preliminary cleanup of these files.

Which one should be reviewed first? Or they're independent?

Sorry this wasn't very clear. As I said in our DM on Zulip (sorry for the lack of transparency) my ultimate plan was to nuke the direct proof of NoZeroDivisors and instead make it use the fact that the order of a product is the sum of the orders (as it's done in the multivariate setup). I have no preference between:

• merging this and then I go behind to cleanup
• I open the series of cleanup PR incorporating the changes made here

But indeed a choice needs to be made.

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[AntoineChambert-Loir]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style