Documentation

Mathlib.Algebra.PEmptyInstances

Instances on pempty #

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

theorem AddSemigroupPEmpty.proof_1 (x : PEmpty) (y : PEmpty) (z : PEmpty) :
x + y + z = x + (y + z)