[Merged by Bors] - feat(RingTheory.Binomial): Add BinomialRing instance for NNRat modules.

[kcaze]

This PR adds an instance of BinomialRing for NNRat modules.

---

[github-actions]

Import summary

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Binomial	941	947	+6 (+0.64%)

[ScottCarnahan]

Your proof doesn't seem to use any special features of the reals besides the fact that k+1 is invertible for all natural numbers k. This seems to suggest you can replace real numbers with something like {R : Type*} [AddCommMonoid R] [Module ℚ≥0 R] [Pow R ℕ].

[github-actions]

PR summary b198045ae1

Import changes

No significant changes to the import graph

---

Declarations diff

+ instance {R : Type*} [AddCommMonoid R] [Module ℚ≥0 R] [Pow R ℕ] : BinomialRing R

You can run this locally as follows

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

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

[kcaze]

@ScottCarnahan Thanks for the suggestion to generalize. I wasn't able to quite get my proof to work with [AddCommMonoid R] [Module ℚ≥0 R] [Pow R ℕ]. My latest commit requires R to be [CommRing R] [CharZero R] [IsLeftCancelMulZero R] [Algebra ℚ R] instead.

[kcaze]

Thanks, this looks much simpler. I think that instead of a $\mathbb{Q}_{\ge 0}$ module we should however specify a $\mathbb{Q}$ module. With [Module ℚ≥0 R] we cannot synthesize a BinomialRing instance for the reals. For example def test := BinomialRing.multichoose (4:ℝ) 2 yields the error

failed to synthesize
  BinomialRing ℝ

Changing all instances of ℚ≥0 to ℚ fixes this.

Arguably, the real issue is that we lack a equivalent to NNReal.instModuleOfReal but for NNRat and Rat. What do you think?

[ScottCarnahan]

This is curious. I see the instance was removed from Mathlib.Algebra.Module.Basic in #11203.

[ScottCarnahan]

By the way, if you don't want boldface text in the PR description, put a blank line between your text and the line with three dashes.

[kcaze]

Great, thank you. I've committed your suggested version to the PR and am happy with waiting for Yaël's PR to fix synthesizing Module ℚ≥0 ℝ to come after this one.

[ScottCarnahan]

It looks good to me. If you want, you can change the name of the Nat_Int section to something more general like Basic_Instances, and put the instance in there.

[kcaze]

Great, I've changed the section to Basic_Instances so I think this is ready to be merged now.

[kcaze]

@ScottCarnahan, sorry for the ping, but does this need a maintainer merge comment to move into the merging queue? Or do I just need to wait for a maintainer to take a look?

[ScottCarnahan]

Sorry I don't have permission to advance it here, but I can start a discussion on Zulip. On an unrelated note, perhaps you should edit the PR description, e.g., change "real" to "NNRat" or "rational"

[jcommelin]

Thanks!

bors d+

[mathlib-bors]

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

[kcaze]

bors r+

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style