mathlib documentation

algebra.punit_instances

@[instance]

Equations
@[instance]

Equations
@[instance]
def punit.semimodule (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