stabilizer of a submodule

Stream: new members

[Paul Nelson]

I wasn't able to find anything like the following in mathlib, but thought I'd ask:

def Subalgebra.stabilizer
  (R : Type) [CommRing R]
  {V : Type} [AddCommGroup V] [Module R V]
  (U : Submodule R V)
  : Subalgebra R (Module.End R V)
  := by sorry

def Subalgebra.mem_stabilizer_iff
  (R : Type) [CommRing R]
  {V : Type} [AddCommGroup V] [Module R V]
  (U : Submodule R V)
  (x : Module.End R V)
  : x ∈ Subalgebra.stabilizer R U ↔ ∀ v ∈ U, x v ∈ U
  := by sorry

[Eric Wieser]

If we had this, I would hope it would be in the generality of an arbitrary action, not just an endomorphism (of course there isn't really any difference, but it would then match the other content on stabilizers)