feat (RingTheory.MvPowerSeries.Inverse)

[AntoineChambert-Loir]

Prove properties of the inverse of a power series over a general Ring.

A power series is a unit iff its constant coefficient is a unit.

If its constant coefficient is not a zero divisor, then a power series is not a zero divisor.

---

[github-actions[bot]]

PR summary 3a4873426d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.MvPowerSeries.Inverse	1086	1097	+11 (+1.01%)
Mathlib.RingTheory.PowerSeries.Inverse	1094	1105	+11 (+1.01%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.LSeries.HurwitzZetaValues	9
7 files Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.PowerSeries.Derivative Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.NumberTheory.ZetaValues Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.RingTheory.PowerSeries.Inverse	11
Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors	961

---

Declarations diff

+ degree_eq_zero_iff + mem_nonZeroDivisors_of_constantCoeff ++ invOfUnit_mul ++ isUnit_iff_constantCoeff

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>

[jcommelin]

Shouldn't the PR title refer to Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors? That's where most of the changes/contributions seem to be.

[AntoineChambert-Loir]

You're right. Having an inverse in the general case was my motivation, but given what was there, all I had to do is proving that constant coeff invertible (or non zero divisor) implies non zero divisor.

[AntoineChambert-Loir]

Perhaps the file NoZeroDivisors should be NonZeroDivisors, given the name of the structure?

Late on, I will prove here that MvPowerSeries satisfies NoZeroDivisors… Either name is fine to me.

[faenuccio]

Perhaps the file NoZeroDivisors should be NonZeroDivisors, given the name of the structure?

Late on, I will prove here that MvPowerSeries satisfies NoZeroDivisors… Either name is fine to me.

Then I agree with this naming.

[faenuccio]

Thanks!

[faenuccio]

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by faenuccio.

[mathlib-bors[bot]]

:v: 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.

[riccardobrasca]

bors r-

[mathlib-bors[bot]]

Canceled.

[riccardobrasca]

We should really fix the bib linter. I think you have to put the reference in alphabetical order wrt to the author manually.

[AntoineChambert-Loir]

The problem with the bib file with that one should not format it by hand, but just execute bibtool…

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style