Instances on pempty

This file collects facts about algebraic structures on the (universe-polymorphic) empty type, e.g. that it is a semigroup.

@[implicit_reducible]

instance SemigroupPEmpty : Semigroup PEmpty

Equations

• SemigroupPEmpty = { mul := fun (x x_1 : PEmpty) => PEmpty.casesOn (fun (t : PEmpty) => x = t → PEmpty) x ⋯, mul_assoc := ⋯ }

@[implicit_reducible]

instance AddSemigroupPEmpty : AddSemigroup PEmpty

Equations

• AddSemigroupPEmpty = { add := fun (x x_1 : PEmpty) => PEmpty.casesOn (fun (t : PEmpty) => x = t → PEmpty) x ⋯, add_assoc := ⋯ }