Diamond with FractionRing of Localization.AtPrime

Stream: mathlib4

[Xavier Roblot]

I think the following is a diamond:

import Mathlib.RingTheory.DedekindDomain.Instances

variable {R S : Type*} [CommRing R] [CommSemiring S] [IsDedekindDomain R] (p : Ideal R) [p.IsPrime]

local notation "Rₚ" => Localization.AtPrime p

instance : FaithfulSMul R Rₚ := sorry

example :
  (OreLocalization.instAlgebra : Algebra Rₚ (FractionRing Rₚ)) =
    (instAlgebraAtPrimeFractionRing _ : Algebra Rₚ (FractionRing Rₚ)) := rfl -- fails

Note that the instance that says that FaithfulSMul R Rₚ is not in Mathlib yet but it is direct to prove (it is proved in #27152 for example).

[Junyan Xu]

docs#instAlgebraAtPrimeFractionRing should probably be an abbrev just like FractionRing.liftAlgebra

[Kevin Buzzard]

Is this related to #21344 ? Just mentioning it because this is definitely a diamond in OreLocalization

[Kevin Buzzard]

Oh no that looks like something different, it's Int-specific

[Xavier Roblot]

I am pinging @Riccardo Brasca who added docs#instAlgebraAtPrimeFractionRing. Riccardo, should we change this instance into an abbrev?

[Riccardo Brasca]

Oh yes, why not!

[Xavier Roblot]

#28551

[Riccardo Brasca]

I am very busy with non lean things, but feel free to ask my review