Skip to content

Commit

Permalink
feat(algebra/field/basic): div_neg_self, neg_div_self (#11438)
Browse files Browse the repository at this point in the history
I think these two lemmas are useful as `simp` lemmas, but they don't
seem to be there already.
  • Loading branch information
jsm28 committed Jan 14, 2022
1 parent 201aeaa commit 22a9f2e
Showing 1 changed file with 6 additions and 0 deletions.
6 changes: 6 additions & 0 deletions src/algebra/field/basic.lean
Expand Up @@ -97,6 +97,12 @@ by simp [neg_div]
lemma neg_div_neg_eq (a b : K) : (-a) / (-b) = a / b :=
by rw [div_neg_eq_neg_div, neg_div, neg_neg]

@[simp] lemma div_neg_self {a : K} (h : a ≠ 0) : a / -a = -1 :=
by rw [div_neg_eq_neg_div, div_self h]

@[simp] lemma neg_div_self {a : K} (h : a ≠ 0) : (-a) / a = -1 :=
by rw [neg_div, div_self h]

@[field_simps] lemma div_add_div_same (a b c : K) : a / c + b / c = (a + b) / c :=
by simpa only [div_eq_mul_inv] using (right_distrib a b (c⁻¹)).symm

Expand Down

0 comments on commit 22a9f2e

Please sign in to comment.