Commit 2022-11-27 04:26 c4adc919

View on Github →

feat(Algebra/Ring/Units): port file (#746) mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7 porting notes: we're missing assoc_rw and simp_rw I think, so I had to work around it for now, but I left a note. Otherwise very smooth.

Estimated changes

added theorem IsUnit.neg
added theorem IsUnit.neg_iff
added theorem IsUnit.sub_iff
added theorem Units.add_divp
added theorem Units.divp_add
added theorem Units.divp_add_divp
added theorem Units.divp_sub
added theorem Units.divp_sub_divp
added theorem Units.neg_divp
added theorem Units.sub_divp