IsDomain (TensorAlgebra)

Stream: mathlib4

[Richard Copley]

Would the instance below be wanted in mathlib4?

import Mathlib.LinearAlgebra.TensorAlgebra.Basis

instance instIsDomain {R : Type*} [CommRing R] [IsDomain R]
    {M : Type*} [AddCommMonoid M] [Module R M] [Module.Free R M] :
      IsDomain (TensorAlgebra R M) := sorry

Code

[Riccardo Brasca]

I don't see any problem with it.

[Richard Copley]

Thanks, I'll create a PR.

[Richard Copley]

#9890