[Merged by Bors] - feat: add to WithVal API

[smmercuri]

Upstream fixes to errors generated in FLT following the refactor of HeightOneSpectrum.adicCompletion in #22055

• add additional instances to WithVal API
• provide WithVal alternative to adicValued_apply

---

[github-actions]

PR summary 98794fd91a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ adicValued_apply'
+ instance {P S : Type*} [Ring S] [CommRing R] [Semiring P] [Module P R] [Module P S]
+ instance {S : Type*} [Ring S] [CommRing R] [Algebra R S] (w : Valuation S Γ₀) :
+ instance {S : Type*} [Ring S] [CommRing R] [Algebra R S] :

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).

[pechersky]

Would it make sense to have the explicit ringHom/Iso between R and WithVal v, and then compose it with the algebraMap R S, so that these instances don't pierce through the defeq?

[smmercuri]

I had a play around with this just now -- I think there's an issue with the composition approach although it's a bit unclear to me why. I think it's got something to do with RingHom.toAlgebra and Algebra.compHom starting from CommSemiring R to infer certain instances, while we have to start at Ring or CommRing (because we need Ring for Valuation), e.g., I get this error when trying to use RingHom.toAlgebra:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  @Distrib.toMul (WithVal v)
    (@NonUnitalNonAssocSemiring.toDistrib (WithVal v) NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring)
inferred
  @Distrib.toMul (WithVal v)
    (@NonUnitalNonAssocSemiring.toDistrib (WithVal v) NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring)

Although maybe I'm missing something here?

[pechersky]

do you have a branch with this attempt? it'd be easier to take a look there.

[smmercuri]

I don't have a branch, just did this locally, but this is what I tried below WithVal.equiv:

instance {S : Type*} [Ring S] [CommRing R] [Algebra R S] :
    Algebra (WithVal v) S := Algebra.compHom (equiv v).symm

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style