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.

source
@[protected, instance]
def punit.add_comm_group  :
add_comm_group punit
Equations
source
@[protected, instance]
def punit.comm_group  :
comm_group punit
Equations
source
@[simp]
theorem punit.zero_eq  :
0 = punit.star
source
@[simp]
theorem punit.one_eq  :
1 = punit.star
source
@[simp]
theorem punit.mul_eq (x y : punit) :
x * y = punit.star
source
@[simp]
theorem punit.add_eq (x y : punit) :
x + y = punit.star
source
@[simp]
theorem punit.div_eq (x y : punit) :
x / y = punit.star
source
@[simp]
theorem punit.sub_eq (x y : punit) :
x - y = punit.star
source
@[simp]
theorem punit.inv_eq (x : punit) :
x⁻¹ = punit.star
source
@[simp]
theorem punit.neg_eq (x : punit) :
-x = punit.star
source
@[protected, instance]
def punit.comm_ring  :
comm_ring punit
Equations
source
@[protected, instance]
def punit.cancel_comm_monoid_with_zero  :
cancel_comm_monoid_with_zero punit
Equations
source
@[protected, instance]
def punit.normalized_gcd_monoid  :
normalized_gcd_monoid punit
Equations
source
@[simp]
theorem punit.gcd_eq (x y : punit) :
gcd x y = punit.star
source
@[simp]
theorem punit.lcm_eq (x y : punit) :
lcm x y = punit.star
source
@[simp]
theorem punit.norm_unit_eq (x : punit) :
norm_unit x = 1
source
@[protected, instance]
def punit.complete_boolean_algebra  :
complete_boolean_algebra punit
Equations
source
@[simp]
theorem punit.top_eq  :
⊤ = punit.star
source
@[simp]
theorem punit.bot_eq  :
⊥ = punit.star
source
@[simp]
theorem punit.sup_eq (x y : punit) :
x ⊔ y = punit.star
source
@[simp]
theorem punit.inf_eq (x y : punit) :
x ⊓ y = punit.star
source
@[simp]
theorem punit.Sup_eq (s : set punit) :
Sup s = punit.star
source
@[simp]
theorem punit.Inf_eq (s : set punit) :
Inf s = punit.star
source
@[simp]
theorem punit.compl_eq (x : punit) :
xᶜ = punit.star
source
@[simp]
theorem punit.sdiff_eq (x y : punit) :
x \ y = punit.star
source
@[protected, simp]
theorem punit.le (x y : punit) :
x ≤ y
source
@[simp]
theorem punit.not_lt (x y : punit) :
¬x < y
source
@[protected, instance]
def punit.canonically_ordered_add_monoid  :
canonically_ordered_add_monoid punit
Equations
source
@[protected, instance]
def punit.linear_ordered_cancel_add_comm_monoid  :
linear_ordered_cancel_add_comm_monoid punit
Equations
source
@[protected, instance]
def punit.has_scalar {R : Type u_1} :
has_scalar R punit
Equations
source
@[simp]
theorem punit.smul_eq {R : Type u_1} (y : punit) (r : R) :
r • y = punit.star
source
@[protected, instance]
def punit.smul_comm_class {R : Type u_1} {S : Type u_2} :
smul_comm_class R S punit
source
@[protected, instance]
def punit.is_scalar_tower {R : Type u_1} {S : Type u_2} [has_scalar R S] :
is_scalar_tower R S punit
source
@[protected, instance]
def punit.smul_with_zero {R : Type u_1} [has_zero R] :
smul_with_zero R punit
Equations
source
@[protected, instance]
def punit.mul_action {R : Type u_1} [monoid R] :
mul_action R punit
Equations
source
@[protected, instance]
def punit.distrib_mul_action {R : Type u_1} [monoid R] :
distrib_mul_action R punit
Equations
source
@[protected, instance]
def punit.mul_distrib_mul_action {R : Type u_1} [monoid R] :
mul_distrib_mul_action R punit
Equations

TODO: provide mul_semiring_action R punit

source
@[protected, instance]
def punit.mul_action_with_zero {R : Type u_1} [monoid_with_zero R] :
mul_action_with_zero R punit
Equations
source
@[protected, instance]
def punit.module {R : Type u_1} [semiring R] :
module R punit
Equations