finite and finitely presented algebra

Stream: Is there code for X?

[Christian Merten]

Do we have something close to the following?

import Mathlib

instance {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Module.Finite R S] [Algebra.FinitePresentation R S] :
    Module.FinitePresentation R S :=
  sorry

i.e. a finitely presented algebra that is finite as a module is also finitely presented as a module.

[Junyan Xu]

Apparently it's not there; it's stacks#0564 as noted in this answer.

[Junyan Xu]

@loogle Algebra.FinitePresentation, Module.FinitePresentation

[loogle]

:search: Algebra.instFinitePresentationKaehlerDifferentialOfFinitePresentation

[Christian Merten]

Junyan Xu said:

Apparently it's not there; it's stacks#0564 as noted in this answer.

Thanks, I also found that reference and this looks quite doable, so I will follow that.