Mathlib.Algebra.Group.PUnit

Module docstring

{"# PUnit is a commutative group

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

PUnit.commGroup instance

: CommGroup PUnit

Full source

@[to_additive]
instance commGroup : CommGroup PUnit where
  mul _ _ := unit
  one := unit
  inv _ := unit
  div _ _ := unit
  npow _ _ := unit
  zpow _ _ := unit
  mul_assoc _ _ _ := rfl
  one_mul _ := rfl
  mul_one _ := rfl
  inv_mul_cancel _ := rfl
  mul_comm _ _ := rfl

Commutative Group Structure on the One-Element Type

Informal description

The one-element type `PUnit` forms a commutative group under the unique possible multiplication operation.

PUnit.instOne instance

: One PUnit

Full source

@[to_additive] instance : One PUnit where one := unit

One-element type as a monoid

Informal description

The one-element type `PUnit` has a canonical structure of a one-element monoid with identity element `*`.

PUnit.instMul_mathlib instance

: Mul PUnit

Full source

@[to_additive] instance : Mul PUnit where mul _ _ := unit

Multiplication on the One-Element Type

Informal description

The one-element type `PUnit` has a canonical multiplication operation.

PUnit.instDiv_mathlib instance

: Div PUnit

Full source

@[to_additive] instance : Div PUnit where div _ _ := unit

Division Operation on the One-Element Type

Informal description

The one-element type `PUnit` is equipped with a division operation.

PUnit.instInv instance

: Inv PUnit

Full source

@[to_additive] instance : Inv PUnit where inv _ := unit

Inversion on the One-Element Type

Informal description

The one-element type `PUnit` has an inversion operation, where the inverse of the unique element is itself.

PUnit.one_eq theorem

: (1 : PUnit) = unit

Full source

@[to_additive (attr := simp)] lemma one_eq : (1 : PUnit) = unit := rfl

Multiplicative Identity in One-Element Type Equals Its Unique Element

Informal description

The multiplicative identity element `1` in the one-element type `PUnit` is equal to its unique element `unit`.

PUnit.mul_eq theorem

(x y : PUnit) : x * y = unit

Full source

@[to_additive] lemma mul_eq (x y : PUnit) : x * y = unit := rfl

Multiplication in One-Element Type Yields Unit

Informal description

For any two elements $x$ and $y$ of the one-element type `PUnit`, their multiplication $x * y$ is equal to the unique element `unit`.

PUnit.div_eq theorem

(x y : PUnit) : x / y = unit

Full source

@[to_additive (attr := simp)] lemma div_eq (x y : PUnit) : x / y = unit := rfl

Division in One-Element Type Yields Unit

Informal description

For any two elements $x$ and $y$ of the one-element type `PUnit`, their division $x / y$ is equal to the unique element `unit`.

PUnit.inv_eq theorem

(x : PUnit) : x⁻¹ = unit

Full source

@[to_additive (attr := simp)] lemma inv_eq (x : PUnit) : x⁻¹ = unit := rfl

Inverse in One-Element Type Equals Unit

Informal description

For any element $x$ of the one-element type `PUnit`, the inverse of $x$ is equal to the unique element `unit`, i.e., $x^{-1} = \text{unit}$.