Commit 2023-03-23 17:36 47a6fc57

View on Github →

chore: fix misported Int.natAbs_sq (#3054) mathlib3 had the coercion inside the power.

Estimated changes

modified theorem Int.natAbs_sq