Instances on pempty #

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 (universe-polymorphic) empty type, e.g. that it is a semigroup.

@[protected, instance]

Equations

add_semigroup_pempty = {add := λ (x y : pempty), pempty.cases_on (λ (x : pempty), pempty) x, add_assoc := add_semigroup_pempty._proof_1}

@[protected, instance]

def semigroup_pempty :

Equations

semigroup_pempty = {mul := λ (x y : pempty), pempty.cases_on (λ (x : pempty), pempty) x, mul_assoc := semigroup_pempty._proof_1}