mathlib3 documentation

algebra.punit_instances

Instances on punit #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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  :
0 = punit.star
@[simp]
theorem punit.one_eq  :
1 = punit.star
@[simp]
theorem punit.mul_eq (x y : punit) :
x * y = punit.star
@[simp]
theorem punit.add_eq (x y : punit) :
x + y = punit.star
@[simp, nolint]
theorem punit.div_eq (x y : punit) :
x / y = punit.star
@[simp, nolint]
theorem punit.sub_eq (x y : punit) :
x - y = punit.star
@[simp, nolint]
theorem punit.inv_eq (x : punit) :
x⁻¹ = punit.star
@[simp, nolint]
theorem punit.neg_eq (x : punit) :
-x = punit.star
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem punit.gcd_eq (x y : punit) :
gcd_monoid.gcd x y = punit.star
@[simp]
theorem punit.lcm_eq (x y : punit) :
gcd_monoid.lcm x y = punit.star
@[protected, instance]
Equations
@[protected, instance]
def punit.has_smul {R : Type u_1} :
Equations
@[protected, instance]
def punit.has_vadd {R : Type u_1} :
Equations
@[simp]
theorem punit.vadd_eq {R : Type u_1} (y : punit) (r : R) :
r +ᵥ y = punit.star
@[simp]
theorem punit.smul_eq {R : Type u_1} (y : punit) (r : R) :
r y = punit.star
@[protected, instance]
@[protected, instance]
@[protected, instance]
def punit.smul_comm_class {R : Type u_1} {S : Type u_2} :
@[protected, instance]
def punit.vadd_comm_class {R : Type u_1} {S : Type u_2} :
@[protected, instance]
def punit.vadd_assoc_class {R : Type u_1} {S : Type u_2} [has_vadd R S] :
@[protected, instance]
def punit.is_scalar_tower {R : Type u_1} {S : Type u_2} [has_smul R S] :
@[protected, instance]
def punit.mul_action {R : Type u_1} [monoid R] :
Equations