# Variations on non-zero divisors in `AddMonoidAlgebra`

s #

This file studies the interaction between typeclass assumptions on two Types `R`

and `A`

and
whether `R[A]`

has non-zero zero-divisors. For some background on related
questions, see Kaplansky's Conjectures,
especially the *zero divisor conjecture*.

*Conjecture.*
Let `K`

be a field, and `G`

a torsion-free group. The group ring `K[G]`

does not contain
nontrivial zero divisors, that is, it is a domain.

In this file we show that if `R`

satisfies `NoZeroDivisors`

and `A`

is a grading type satisfying
`UniqueProds A`

(resp. `UniqueSums A`

), then `MonoidAlgebra R A`

(resp. `R[A]`

)
also satisfies `NoZeroDivisors`

.

Because of the instances to `UniqueProds/Sums`

, we obtain a formalization of the well-known result
that if `R`

is a field and `A`

is a left-ordered group, then `R[A]`

contains no non-zero
zero-divisors.
The actual assumptions on `R`

are weaker.

## Main results #

`MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul`

and`AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd`

general sufficient results stating that certain monomials in a product have as coefficient a product of coefficients of the factors.- The instance showing that
`Semiring R, NoZeroDivisors R, Mul A, UniqueProds A`

imply`NoZeroDivisors (MonoidAlgebra R A)`

. - The instance showing that
`Semiring R, NoZeroDivisors R, Add A, UniqueSums A`

imply`NoZeroDivisors R[A]`

.

TODO: move the rest of the docs to UniqueProds?
`NoZeroDivisors.of_left_ordered`

shows that if `R`

is a semiring with no non-zero
zero-divisors, `A`

is a linearly ordered, add right cancel semigroup with strictly monotone
left addition, then `R[A]`

has no non-zero zero-divisors.

`NoZeroDivisors.of_right_ordered`

shows that if`R`

is a semiring with no non-zero zero-divisors,`A`

is a linearly ordered, add left cancel semigroup with strictly monotone right addition, then`R[A]`

has no non-zero zero-divisors.

The conditions on `A`

imposed in `NoZeroDivisors.of_left_ordered`

are sometimes referred to as
`left-ordered`

.
The conditions on `A`

imposed in `NoZeroDivisors.of_right_ordered`

are sometimes referred to as
`right-ordered`

.

These conditions are sufficient, but not necessary. As mentioned above, *Kaplansky's Conjecture*
asserts that `A`

being torsion-free may be enough.

The coefficient of a monomial in a product `f * g`

that can be reached in at most one way
as a product of monomials in the supports of `f`

and `g`

is a product.

## Equations

- ⋯ = ⋯

The coefficient of a monomial in a product `f * g`

that can be reached in at most one way
as a product of monomials in the supports of `f`

and `g`

is a product.

## Equations

- ⋯ = ⋯