Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 988f160

Browse files
author
Jon Eugster
committed
fix(data/rat/basic): Remove incorrect simp attribute (#14765)
Remove simp attribute that breaks `field_simp`.
1 parent 6c46641 commit 988f160

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/data/rat/basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -675,7 +675,7 @@ by rw [div_eq_mul_inv, inv_def, mk_mul_mk_cancel hx]
675675
lemma mk_div_mk_cancel_right {x : ℤ} (hx : x ≠ 0) (n d : ℤ) : (x /. n) / (x /. d) = d /. n :=
676676
by rw [div_eq_mul_inv, inv_def, mul_comm, mk_mul_mk_cancel hx]
677677

678-
@[simp] lemma coe_int_div_eq_mk {n d : ℤ} : (n : ℚ) / ↑d = n /. d :=
678+
lemma coe_int_div_eq_mk {n d : ℤ} : (n : ℚ) / ↑d = n /. d :=
679679
begin
680680
repeat {rw coe_int_eq_mk},
681681
exact mk_div_mk_cancel_left one_ne_zero n d,

0 commit comments

Comments
 (0)