Commit 2022-11-28 16:05 41c68329

View on Github →

feat(Algebra/Regular/Basic): port file (#758) mathlib SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636 Porting notes:

  1. It seems like to_additive is not correctly converting IsLeftRegular, IsRightRegular, and IsRegular. Giving explicit names for their conversion fixes this issue.
  2. The proof of IsLeftRegular.ne_zero needed an additional type annotation to behave properly

Estimated changes

added theorem Commute.isRegular_iff
added structure IsAddRegular
added theorem IsLeftRegular.mul
added theorem IsLeftRegular.ne_zero
added theorem IsLeftRegular.of_mul
added def IsLeftRegular
added theorem IsRegular.ne_zero
added theorem IsRegular.subsingleton
added structure IsRegular
added theorem IsRightRegular.mul
added theorem IsRightRegular.ne_zero
added theorem IsRightRegular.of_mul
added def IsRightRegular
added theorem IsUnit.isRegular
added theorem Units.isRegular
added theorem isRegular_iff_ne_zero
added theorem isRegular_mul_iff
added theorem isRegular_of_ne_zero
added theorem isRegular_one
added theorem mul_isLeftRegular_iff
added theorem mul_isRightRegular_iff
added theorem not_isLeftRegular_zero
added theorem not_isRegular_zero