Commit 2024-03-29 22:03 9e78f5c2
View on Github →chore: remove Complex/RCLike bit0/1 lemmas (#11414) These were interesting when they worked on number literals, which is no longer the case in lean4.
chore: remove Complex/RCLike bit0/1 lemmas (#11414) These were interesting when they worked on number literals, which is no longer the case in lean4.