Skip to content

Commit

Permalink
refactor(algebra/group/basic): simp -> rw in `sub_eq_sub_iff_sub_eq_s…
Browse files Browse the repository at this point in the history
…ub` (#5903)

co-authors: `lean-gptf`, Yuhuai Wu
  • Loading branch information
Jesse Michael Han committed Jan 27, 2021
1 parent 1cd2286 commit fd55e57
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/algebra/group/basic.lean
Expand Up @@ -544,6 +544,6 @@ begin
end

lemma sub_eq_sub_iff_sub_eq_sub : a - b = c - d ↔ a - c = b - d :=
by simp [-sub_eq_add_neg, sub_eq_sub_iff_add_eq_add, add_comm]
by rw [sub_eq_iff_eq_add, sub_add_eq_add_sub, sub_eq_iff_eq_add', add_sub_assoc]

end add_comm_group

0 comments on commit fd55e57

Please sign in to comment.