-
Notifications
You must be signed in to change notification settings - Fork 251
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(Algebra/GroupWithZero/Units/Basic): port file #735
Conversation
…roup_with_zero.units.basic
I think this is good to go |
This PR should be ready now. |
bors merge |
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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following PRs: * `algebra.field.defs`: leanprover-community/mathlib4#668 * `algebra.group.commute`: leanprover-community/mathlib4#750 * `algebra.group_with_zero.commute`: leanprover-community/mathlib4#762 * `algebra.group_with_zero.semiconj`: leanprover-community/mathlib4#757 * `algebra.group_with_zero.units.basic`: leanprover-community/mathlib4#735 * `algebra.hom.embedding`: leanprover-community/mathlib4#764 * `algebra.order.monoid.cancel.defs`: leanprover-community/mathlib4#774 * `algebra.order.monoid.canonical.defs`: leanprover-community/mathlib4#778 * `algebra.order.monoid.defs`: leanprover-community/mathlib4#771 * `algebra.order.monoid.min_max`: leanprover-community/mathlib4#763 * `algebra.order.monoid.order_dual`: leanprover-community/mathlib4#786 * `algebra.order.sub.defs`: leanprover-community/mathlib4#732 * `algebra.regular.basic`: leanprover-community/mathlib4#758 * `algebra.ring.commute`: leanprover-community/mathlib4#759 * `algebra.ring.regular`: leanprover-community/mathlib4#795 * `algebra.ring.semiconj`: leanprover-community/mathlib4#751 * `control.applicative`: leanprover-community/mathlib4#798 * `control.functor`: leanprover-community/mathlib4#612 * `control.monad.basic`: leanprover-community/mathlib4#752 * `data.countable.defs`: leanprover-community/mathlib4#736 * `data.int.units`: leanprover-community/mathlib4#807 * `data.nat.basic`: leanprover-community/mathlib4#729 * `data.nat.psub`: leanprover-community/mathlib4#806 * `data.nat.units`: leanprover-community/mathlib4#805 * `data.pi.algebra`: leanprover-community/mathlib4#564 * `data.prod.lex`: leanprover-community/mathlib4#783 * `logic.embedding.basic`: leanprover-community/mathlib4#700 * `logic.equiv.option`: leanprover-community/mathlib4#674 * `order.bounded_order`: leanprover-community/mathlib4#697 * `order.with_bot`: leanprover-community/mathlib4#776 * `order.disjoint`: leanprover-community/mathlib4#773 * `order.min_max`: leanprover-community/mathlib4#728 * `order.prop_instances`: leanprover-community/mathlib4#792 * `order.rel_iso.basic`: leanprover-community/mathlib4#772
mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7
porting notes:
mul_inv_cancel
has an extra explicit argument now (from another file that was ported); does this need to be fixed? (FIXED)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.)protected
attribute to the aliasNe.isUnit
(add protected after the fact? #740)AssertExists
or ratherAssertNotExists
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.simp
lemmas now trip thesimpNF
linter because they involve coercions and can be proven bysimp
already, so I removed thesimp
attribute.