Skip to content

Commit 47a6fc5

Browse files
chore: fix misported Int.natAbs_sq (#3054)
[mathlib3](https://leanprover-community.github.io/mathlib_docs/algebra/group_power/lemmas.html#int.nat_abs_sq) had the coercion inside the power.
1 parent b1d3f2c commit 47a6fc5

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/Algebra/GroupPower/Lemmas.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -733,7 +733,7 @@ end LinearOrderedRing
733733

734734
namespace Int
735735

736-
lemma natAbs_sq (x : ℤ) : (x.natAbs ^ 2) = x ^ 2 := by rw [sq, Int.natAbs_mul_self, sq]
736+
lemma natAbs_sq (x : ℤ) : (x.natAbs : ℤ) ^ 2 = x ^ 2 := by rw [sq, Int.natAbs_mul_self', sq]
737737
#align int.nat_abs_sq Int.natAbs_sq
738738

739739
alias natAbs_sq ← natAbs_pow_two

0 commit comments

Comments
 (0)