Commit 2024-02-05 11:50 6d578c58

View on Github →

feat: tensor algebra of free module over integral domain is a domain (#9890) Provide instances

  • Nontrivial (TensorAlgebra R M) when M is a module over a nontrivial semiring R
  • NoZeroDivisors (FreeAlgebra R X) when R is a commutative semiring with no zero-divisors and X any type
  • IsDomain (FreeAlgebra R X) when R is an integral domain and X is any type
  • TwoUniqueProds (FreeMonoid X) where X is any type (this provides NoZeroDivisors (MonoidAlgebra R (FreeMonoid X)) when R is a semiring and X any type, via TwoUniqueProds.toUniqueProds and MonoidAlgebra.instNoZeroDivisorsOfUniqueProds)
  • NoZeroDivisors (TensorAlgebra R M) when M is a free module over a commutative semiring R with no zero-divisors
  • IsDomain (TensorAlgebra R M) when M is a free module over an integral domain R In Algebra.Group.UniqueProds:
  • Rename UniqueProds.mulHom_image_of_injective to UniqueProds.of_injective_mulHom.
  • New lemmas UniqueMul.of_mulHom_image, UniqueProds.of_mulHom, TwoUniqueProds.of_mulHom show the relevant property holds in the domain of a multiplicative homomorphism if it holds in the codomain, under a certain hypothesis on the homomorphism.

Estimated changes

added theorem UniqueProds.of_mulHom
modified theorem Finset.nontrivial_prod_iff