∀ {α : Type u_1} {R : Type u_2} [inst : Add R] [inst_1 : MulOneClass R] [inst_2 : SMul α R]
  [inst_3 : IsScalarTower α R R] (c : RingCon R) [inst_4 : SMul αᵐᵒᵖ R] [inst_5 : IsCentralScalar α R],
  IsCentralScalar α c.Quotient