[Merged by Bors] - feat(Algebra/GroupWithZero/Units/Basic): port file#735
Closed
[Merged by Bors] - feat(Algebra/GroupWithZero/Units/Basic): port file#735
Conversation
…roup_with_zero.units.basic
kim-em
reviewed
Nov 26, 2022
eric-wieser
reviewed
Nov 26, 2022
Contributor
|
I think this is good to go |
Contributor
Author
|
This PR should be ready now. |
Contributor
|
bors merge |
bors bot
pushed a commit
that referenced
this pull request
Nov 27, 2022
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: |
bors bot
pushed a commit
to leanprover-community/mathlib3
that referenced
this pull request
Dec 1, 2022
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
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7
porting notes:
mul_inv_cancelhas 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.)protectedattribute to the aliasNe.isUnit(add protected after the fact? #740)AssertExistsor ratherAssertNotExistsis 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.simplemmas now trip thesimpNFlinter because they involve coercions and can be proven bysimpalready, so I removed thesimpattribute.