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.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem punit.zero_eq  :
@[simp]
theorem punit.one_eq  :
@[simp]
theorem punit.mul_eq (x y : punit) :
@[simp]
theorem punit.add_eq (x y : punit) :
@[simp]
theorem punit.div_eq (x y : punit) :
@[simp]
theorem punit.sub_eq (x y : punit) :
@[simp]
theorem punit.inv_eq (x : punit) :
@[simp]
theorem punit.neg_eq (x : punit) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem punit.gcd_eq (x y : punit) :
@[simp]
theorem punit.lcm_eq (x y : punit) :
@[simp]
theorem punit.norm_unit_eq (x : punit) :
@[protected, instance]
Equations
@[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.compl_eq (x : punit) :
@[simp]
theorem punit.sdiff_eq (x y : punit) :
@[protected, simp]
theorem punit.le (x y : punit) :
x y
@[simp]
theorem punit.not_lt (x y : punit) :
¬x < y
@[protected, instance]
Equations
@[protected, instance]
def punit.has_scalar {R : Type u_1} :
Equations
@[simp]
theorem punit.smul_eq {R : Type u_1} (y : punit) (r : R) :
@[protected, instance]
def punit.smul_comm_class {R : Type u_1} {S : Type u_2} :
@[protected, instance]
def punit.is_scalar_tower {R : Type u_1} {S : Type u_2} [has_scalar R S] :
@[protected, instance]
def punit.smul_with_zero {R : Type u_1} [has_zero R] :
Equations
@[protected, instance]
def punit.mul_action {R : Type u_1} [monoid R] :
Equations

TODO: provide mul_semiring_action R punit