A commutative semiring that is a domain whose polynomial semiring is not a domain

NatMaxAdd is the natural numbers equipped with the usual multiplication but with maximum as addition. Under these operations it is a commutative semiring that is a domain, but 1 + 1 = 1 + 0 = 1 in this semiring so addition is not cancellative. As a consequence, the polynomial semiring NatMaxAdd[X] is not a domain, even though it has no zero-divisors other than 0.

@[irreducible]

def NatMaxAdd : Type

A type synonym for ℕ equipped with maximum as addition.

Equations

• NatMaxAdd = ℕ

@[reducible, inline]

abbrev NatMaxAdd.mk : ℕ ≃ NatMaxAdd

Identification of NatMaxAdd with ℕ.

Equations

• NatMaxAdd.mk = Equiv.refl ℕ

instance NatMaxAdd.instAddCommSemigroup : AddCommSemigroup NatMaxAdd

Equations

• One or more equations did not get rendered due to their size.

instance NatMaxAdd.instAddZeroClass : AddZeroClass NatMaxAdd

Equations

• One or more equations did not get rendered due to their size.

instance NatMaxAdd.instCommMonoidWithZero : CommMonoidWithZero NatMaxAdd

Equations

• NatMaxAdd.instCommMonoidWithZero = NatMaxAdd.mk.symm.commMonoidWithZero

def NatMaxAdd.mulEquiv : NatMaxAdd ≃* ℕ

NatMaxAdd is isomorphic to ℕ multiplicatively.

Equations

• NatMaxAdd.mulEquiv = { toEquiv := NatMaxAdd.mk.symm, map_mul' := NatMaxAdd.mulEquiv._proof_1 }

instance NatMaxAdd.instCommSemiring : CommSemiring NatMaxAdd

Equations

• One or more equations did not get rendered due to their size.

instance NatMaxAdd.instIsDomain : IsDomain NatMaxAdd

theorem NatMaxAdd.natCast_eq_one (n : ℕ) [NeZero n] : ↑n = 1

theorem NatMaxAdd.not_isCancelAdd : ¬IsCancelAdd NatMaxAdd

theorem NatMaxAdd.not_isDomain_polynomial : ¬IsDomain (Polynomial NatMaxAdd)

theorem NatMaxAdd.noZeroDivisors_polynomial : NoZeroDivisors (Polynomial NatMaxAdd)

theorem not_isDomain_commSemiring_imp_isDomain_polynomial : ¬∀ (R : Type) [inst : CommSemiring R] [IsDomain R], IsDomain (Polynomial R)