Commit 2023-03-08 11:50 cc47ebbf

View on Github →

refactor: change defeqs of pow and zsmul on UInt, golf the ring instance (#2567) This now makes these operators have the obvious defeq WRT the underlying Fin size, rather than compute things iteratively.

Estimated changes

Modified Mathlib/Data/UInt.lean

added theorem $typeName.intCast_def

added theorem $typeName.natCast_def

added theorem $typeName.nsmul_def

added theorem $typeName.pow_def

added theorem $typeName.val_injective

added theorem $typeName.zsmul_def