mathlib documentation

core / init.data.punit

theorem punit_eq (a b : punit) :
a = b

theorem punit_eq_star (a : punit) :

@[instance]

Equations