Generalizing `MvPolynomial.finSuccEquiv`?

Stream: mathlib4

[Quang Dao]

docs#MvPolynomial.finSuccEquiv is an algebra equivalence between R[X_0, ..., X_n] and R[X_1,..., X_n][X_0]. For my purpose, I want to generalize this an arbitrary pivot p : Fin (n + 1) and not just p = 0.

This leads to the following natural definition:

import Mathlib.Algebra.MvPolynomial.Equiv

def MvPolynomial.finSuccEquiv' (p : Fin (n + 1)) :
    MvPolynomial (Fin (n + 1)) R ≃ₐ[R] Polynomial (MvPolynomial (Fin n) R) :=
  (renameEquiv R (_root_.finSuccEquiv' p)).trans (optionEquivLeft R (Fin n))

which just replaces docs#finSuccEquiv with its general version docs#finSuccEquiv'.

This is perfectly fine to me, but @Yaël Dillies suggested that we could aim for an even more general version with arbitrary types, like so:

import Mathlib

def MvPolynomial.singletonComplEquiv {α β : Type*} (f : α → β) (b : β) (h : Set.range f = {b}ᶜ) :
    MvPolynomial β R ≃ₐ[R] Polynomial (MvPolynomial α R) :=
  -- A crude attempt to define the equivalence
  have βEquiv : β ≃ {x : β // x = b} ⊕ {x : β // x ≠ b} := sorry
  have {R : Type*} [CommSemiring R] (γ : Type*) [Unique γ] :
    MvPolynomial γ R ≃ₐ[R] Polynomial R := sorry
  (renameEquiv R βEquiv).trans ((sumAlgEquiv R _ _).trans (this { x // x = b }))

Should I define this more general version or stick to the more concrete setting of docs#finSuccEquiv'?

[Eric Wieser]

Do we have the Option version already?

[Quang Dao]

Yes you're right, I also realized after posting this.