{R : Type u_1} →
  {M₁ : Type u_2} →
    {M₂ : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                (Q₁ : QuadraticForm R M₁) →
                  (Q₂ : QuadraticForm R M₂) →
                    CliffordAlgebra (QuadraticMap.prod Q₁ Q₂) ≃ₐ[R]
                      GradedTensorProduct R (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂)