Commit 2022-11-27 22:58 de9b4864

feat(Algebra/GroupWithZero/Units/Basic): port file (#735) mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7 porting notes:

1. mul_inv_cancel has an extra explicit argument now (from another file that was ported); does this need to be fixed? (FIXED)
2. I'm worried about the proof of Units.mul_inv' because it suggests to me that something is wrong, but maybe this is a result of how casts are handled now? We should look into it. (FIXED: the issue was that Lean 4 elaborated the theorem statement differently than Lean 3, so the lemma was actually invisibly stated incorrectly; the fix was to help the elaborator to produce the right statement.)
3. A few other proofs required trivial fixes, but it's a bit surprising they needed them.
4. I couldn't seem to add the protected attribute to the alias Ne.isUnit (#740)
5. It seems that AssertExists or rather AssertNotExists is not implemented yet in mathlib4, so we can't use it to guard against import creep at the bottom of the file, but I think this is fine for now.
6. A few simp lemmas now trip the simpNF linter because they involve coercions and can be proven by simp already, so I removed the simp attribute.