∀ {R : Type u_3} {B : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }),
  (∀ (x y : A),
      ((↑fe).1, MulOpposite.op (↑fe).2 • (↑fe).1.toLinearMap).2 x *
          ((↑fe).1, MulOpposite.op (↑fe).2 • (↑fe).1.toLinearMap).2 y =
        0) ∧
    (∀ (r x : A),
        ((↑fe).1, MulOpposite.op (↑fe).2 • (↑fe).1.toLinearMap).2 (r • x) =
          ((↑fe).1, MulOpposite.op (↑fe).2 • (↑fe).1.toLinearMap).1 r *
            ((↑fe).1, MulOpposite.op (↑fe).2 • (↑fe).1.toLinearMap).2 x) ∧
      ∀ (r x : A),
        ((↑fe).1, MulOpposite.op (↑fe).2 • (↑fe).1.toLinearMap).2 (MulOpposite.op r • x) =
          ((↑fe).1, MulOpposite.op (↑fe).2 • (↑fe).1.toLinearMap).2 x *
            ((↑fe).1, MulOpposite.op (↑fe).2 • (↑fe).1.toLinearMap).1 r