[Merged by Bors] - feat(Algebra/GroupWithZero): remove already existing lemmas

[pitmonticone]

Undo #11677 since we have found out that the lemmas

mathlib4/Mathlib/Algebra/GroupWithZero/Divisibility.lean

Lines 171 to 179 in 044f133

	lemma dvd_of_mul_dvd_mul_left {c : α} (hc : c ≠ 0)
	(H : c * a ∣ c * b) : a ∣ b := by
	rcases H with ⟨d, hd⟩
	exact ⟨d, by simpa [mul_assoc, hc] using hd⟩
	lemma dvd_of_mul_dvd_mul_right {c : α} (hc : c ≠ 0)
	(H : a * c ∣ b * c) : a ∣ b := by
	rw [mul_comm a c, mul_comm b c] at H
	exact dvd_of_mul_dvd_mul_left hc H

already exist in the same file with different names mul_dvd_mul_iff_left and mul_dvd_mul_iff_right:

mathlib4/Mathlib/Algebra/GroupWithZero/Divisibility.lean

Lines 46 to 58 in 0f2ac67

	/-- Given two elements `b`, `c` of a `CancelMonoidWithZero` and a nonzero element `a`,
	`a*b` divides `a*c` iff `b` divides `c`. -/
	theorem mul_dvd_mul_iff_left [CancelMonoidWithZero α] {a b c : α} (ha : a ≠ 0) :
	a * b ∣ a * c ↔ b ∣ c :=
	exists_congr fun d => by rw [mul_assoc, mul_right_inj' ha]
	#align mul_dvd_mul_iff_left mul_dvd_mul_iff_left
	/-- Given two elements `a`, `b` of a commutative `CancelMonoidWithZero` and a nonzero
	element `c`, `a*c` divides `b*c` iff `a` divides `b`. -/
	theorem mul_dvd_mul_iff_right [CancelCommMonoidWithZero α] {a b c : α} (hc : c ≠ 0) :
	a * c ∣ b * c ↔ a ∣ b :=
	exists_congr fun d => by rw [mul_right_comm, mul_left_inj' hc]
	#align mul_dvd_mul_iff_right mul_dvd_mul_iff_right

[riccardobrasca]

Oh gosh. We want these to have the same name as the Int and Nat version (that are in Std I think).

[riccardobrasca]

Ah sorry, these already match the names in Std, but we were looking for only one implication.

[pitmonticone]

@riccardobrasca Yes, exactly.

[fpvandoorn]

Thanks!

bors d+

[mathlib-bors]

✌️ pitmonticone can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[pitmonticone]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style