# Examples of zero-divisors in `AddMonoidAlgebra`

s #

This file contains an easy source of zero-divisors in an `AddMonoidAlgebra`

.
If `k`

is a field and `G`

is an additive group containing a non-zero torsion element, then
`k[G]`

contains non-zero zero-divisors: this is lemma `zero_divisors_of_torsion`

.

There is also a version for periodic elements of an additive monoid: `zero_divisors_of_periodic`

.

The converse of this statement is Kaplansky's zero divisor conjecture.

The formalized example generalizes in trivial ways the assumptions: the field `k`

can be any
nontrivial ring `R`

and the additive group `G`

with a torsion element can be any additive monoid
`A`

with a non-zero periodic element.

Besides this example, we also address a comment in `Data.Finsupp.Lex`

to the effect that the proof
that addition is monotone on `α →₀ N`

uses that it is *strictly* monotone on `N`

.

The specific statement is about `Finsupp.Lex.covariantClass_lt_left`

and its analogue
`Finsupp.Lex.covariantClass_le_right`

. We do not need two separate counterexamples, since the
operation is commutative.

The example is very simple. Let `F = {0, 1}`

with order determined by `0 < 1`

and absorbing
addition (which is the same as `max`

in this case). We denote a function `f : F → F`

(which is
automatically finitely supported!) by `[f 0, f 1]`

, listing its values. Recall that the order on
finitely supported function is lexicographic, matching the list notation. The inequality
`[0, 1] ≤ [1, 0]`

holds. However, adding `[1, 0]`

to both sides yields the *reversed* inequality
`[1, 1] > [1, 0]`

.

This is a simple example showing that if `R`

is a non-trivial ring and `A`

is an additive
monoid with an element `a`

satisfying `n • a = a`

and `(n - 1) • a ≠ a`

, for some `2 ≤ n`

,
then `R[A]`

contains non-zero zero-divisors. The elements are easy to write down:
`[a]`

and `[a] ^ (n - 1) - 1`

are non-zero elements of `R[A]`

whose product
is zero.

Observe that such an element `a`

*cannot* be invertible. In particular, this lemma never applies
if `A`

is a group.

This is a simple example showing that if `R`

is a non-trivial ring and `A`

is an additive
monoid with a non-zero element `a`

of finite order `oa`

, then `R[A]`

contains
non-zero zero-divisors. The elements are easy to write down:
`∑ i in Finset.range oa, [a] ^ i`

and `[a] - 1`

are non-zero elements of `R[A]`

whose product is zero.

In particular, this applies whenever the additive monoid `A`

is an additive group with a non-zero
torsion element.

- zero: Counterexample.F
- one: Counterexample.F

`F`

is the type with two elements `zero`

and `one`

. We define the "obvious" linear order and
absorbing addition on it to generate our counterexample.

## Instances For

The same as `List.getRest`

, except that we take the "rest" from the first match, rather than
from the beginning, returning `[]`

if there is no match. For instance,

```
#eval dropUntil [1,2] [3,1,2,4,1,2] -- [4, 1, 2]
```

## Equations

- Counterexample.List.dropUntil x [] = []
- Counterexample.List.dropUntil x (a :: as) = Option.getD (List.getRest (a :: as) x) (Counterexample.List.dropUntil x as)

## Instances For

`guard_decl na mod`

makes sure that the declaration with name `na`

is in the module `mod`

.

```
guard_decl Nat.nontrivial Mathlib.Data.Nat.Basic -- does nothing
guard_decl Nat.nontrivial Not.In.Here
-- the module Not.In.Here is not imported!
```

This test makes sure that the comment referring to this example is in the file claimed in the doc-module to this counterexample.

## Instances For

`1`

is not really needed, but it is nice to use the notation.

A tactic to prove trivial goals by enumeration.

## Instances For

`F`

would be a `CommSemiring`

, using `min`

as multiplication. Again, we do not need this.

The `CovariantClass`

es asserting monotonicity of addition hold for `F`

.

A few `simp`

-lemmas to take care of trivialities in the proof of the example below.