PR summary 18a09f9093

Import changes for modified files

No significant changes to the import graph

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

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

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

I understand that this is a very neat direct proof. But would it be better to first construct the inverse for p = 0+x+O(x^2)? Then presumably you can use "universal polynomials" like they did when defining WittVector.wittAdd? (both of these might be not desirable)

Do you mean constructing the inverse to the power series $$\sum a_k X^k \in R[[X, a_1, a_2,\dots]]$$ and then specialize?

Yes but I think I still want a1=1 here.

It is easy to get what you are describing from what I already have by plugging in R = MvPolynomial Nat R; but I'm not sure what benefits you will get from this?

ah I should have been more clear. I think from doing 0+x+O(x^2) first you get the benefit of not having to use 1/, so the proofs should be "easier"?

Can you add a variant assuming IsUnit? Thanks!

Can you add a variant assuming IsUnit? Thanks!

I am happy to add a variant assuming IsUnit in later PRs. I talked Andrew to pick up this PR (which he did not plan to do it recently) since I will need it. If Andrew @erdOne don't mind, I was wondering whether I can take over this PR. Thanks!

There's nothing wrong with this PR, let's just merge it and others can add variants later.

bors merge

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step