Commit 2022-11-28 16:57 716300ab

View on Github →

feat(Algebra/GroupWithZero/Commute): port file (#762) mathlib3 SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636 porting notes: easy

There were two lemmas that had been ad hoc ported into Algebra.Ring.Basic, which caused these to be marked as dubious translations by Mathport (because the type class assumptions didn't match), so I have just #aligned them without an ₓ here.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/GroupWithZero/Commute.lean

added theorem Commute.div_left

added theorem Commute.div_right

added theorem Commute.inv_left_iff₀

added theorem Commute.inv_left₀

added theorem Commute.inv_right_iff₀

added theorem Commute.inv_right₀

added theorem Commute.ring_inverse_ring_inverse

added theorem Commute.zero_left

added theorem Commute.zero_right

added theorem Ring.mul_inverse_rev'

added theorem Ring.mul_inverse_rev

Modified Mathlib/Algebra/Ring/Basic.lean

deleted theorem Commute.zero_left

deleted theorem Commute.zero_right