mathlib documentation

algebra.punit_instances

Instances on punit #

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

@[instance]
Equations
@[instance]
Equations
@[instance]
def punit.module (R : Type u) [semiring R] :
Equations
@[simp]
theorem punit.zero_eq  :
@[simp]
theorem punit.one_eq  :
@[simp]
theorem punit.add_eq (x y : punit) :
@[simp]
theorem punit.mul_eq (x y : punit) :
@[simp]
theorem punit.div_eq (x y : punit) :
@[simp]
theorem punit.sub_eq (x y : punit) :
@[simp]
theorem punit.neg_eq (x : punit) :
@[simp]
theorem punit.inv_eq (x : punit) :
theorem punit.smul_eq (x y : punit) :
@[simp]
@[simp]
@[simp]
theorem punit.sup_eq (x y : punit) :
@[simp]
theorem punit.inf_eq (x y : punit) :
@[simp]
theorem punit.Sup_eq (s : set punit) :
@[simp]
theorem punit.Inf_eq (s : set punit) :
@[simp]
theorem punit.le (x y : punit) :
x y
@[simp]
theorem punit.not_lt (x y : punit) :
¬x < y