mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

chore: remove Complex/RCLike bit0/1 lemmas

Open Ruben-VandeVelde opened this issue 1 year ago • 2 comments
trafficstars

These were interesting when they worked on number literals, which is no longer the case in lean4.


Open in Gitpod

Ruben-VandeVelde avatar Mar 15 '24 22:03 Ruben-VandeVelde