Skip to content

Commit 57d3dee

Browse files
committed
feat(Algebra/Order/Ring/Unbundled/Rat): rename abs_num_eq_num_natAbs -> abs_num_eq_num_abs
1 parent 36e1240 commit 57d3dee

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

  • Mathlib/Algebra/Order/Ring/Unbundled

Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -147,7 +147,7 @@ theorem abs_def' (q : ℚ) :
147147
(refine ext ?_ ?_ <;> dsimp only; rw [Int.abs_eq_natAbs]) <;>
148148
rw [abs_def, ← Rat.mk_eq_divInt q.num.natAbs _ q.den_ne_zero q.reduced]
149149

150-
theorem abs_num_eq_num_natAbs (q : ℚ) : |q|.num = |q.num| := by
150+
theorem abs_num_eq_num_abs (q : ℚ) : |q|.num = |q.num| := by
151151
rw [abs_def']
152152

153153
theorem abs_den_eq_den (q : ℚ) : |q|.den = q.den := by

0 commit comments

Comments
 (0)