∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : DecidableEq (Module.End R M)] [inst_4 : IsSimpleModule R M] (a b : Module.End R M),
  a / b = a * if h : b = 0 then 0 else ↑(LinearEquiv.ofBijective b ⋯).symm