Commit 2023-12-15 14:16 8aa9689f

View on Github →

feat(Data/Sign): add missing API lemmas (#9074) This adds three simp and norm_cast lemmas for SignType.

Estimated changes

added theorem SignType.coe_mul
added theorem SignType.coe_pow
added theorem SignType.coe_zpow