∀ {R : Type u_3} {P : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra R S] (f : P →ₐ[R] S),
  RingHom.ker f ^ 2 = ⊥ →
    ∀ (g : S →ₐ[R] P) (hg : f.comp g = AlgHom.id R S) (a b : P),
      { toFun := fun x => ⟨x - g (f x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } (a * b) =
        a • { toFun := fun x => ⟨x - g (f x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } b +
          b • { toFun := fun x => ⟨x - g (f x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } a