Mathlib.Algebra.Ring.PUnit

Module docstring

{"# PUnit is a commutative ring

This file collects facts about algebraic structures on the one-element type, e.g. that it is a commutative ring. "}

PUnit.commRing instance

: CommRing PUnit

Full source

instance commRing : CommRing PUnit where
  __ := PUnit.commGroup
  __ := PUnit.addCommGroup
  left_distrib := by intros; rfl
  right_distrib := by intros; rfl
  zero_mul := by intros; rfl
  mul_zero := by intros; rfl
  natCast _ := unit

Commutative Ring Structure on the One-Element Type

Informal description

The one-element type `PUnit` forms a commutative ring under the unique possible operations of addition and multiplication.

PUnit.cancelCommMonoidWithZero instance

: CancelCommMonoidWithZero PUnit

Full source

instance cancelCommMonoidWithZero : CancelCommMonoidWithZero PUnit where
  mul_left_cancel_of_ne_zero := by simp

Cancelative Commutative Monoid with Zero Structure on the One-Element Type

Informal description

The one-element type `PUnit` is a cancelative commutative monoid with zero, meaning it satisfies the properties of a commutative monoid with zero where multiplication by any non-zero element is injective (though in this case, the only element is zero).