Skip to content

feat: Match mathlib#16761#840

Merged
kim-em merged 2 commits intomasterfrom
mul_le_mul_iff_of_ge
Dec 4, 2022
Merged

feat: Match mathlib#16761#840
kim-em merged 2 commits intomasterfrom
mul_le_mul_iff_of_ge

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Dec 3, 2022 •
edited by Ruben-VandeVelde
Loading

I cannot figure out why this fails, but I'm sure someone will :^)

See leanprover-community/mathlib3#16761.

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 3, 2022

Like the error message says, there is no refl tactic. It is called rfl now.

Ruben-VandeVelde
Ruben-VandeVelde reviewed Dec 3, 2022
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 4, 2022

bors d+

Please merge once the mathlib3 PR is approved.

@bors
Copy link
Copy Markdown

bors bot commented Dec 4, 2022

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Dec 4, 2022
@kim-em kim-em merged commit e6628dd into master Dec 4, 2022
@bors bors bot deleted the mul_le_mul_iff_of_ge branch December 4, 2022 02:05
rosborn added a commit that referenced this pull request Dec 4, 2022
@rosborn
Merge branch 'master' into CategoryTheory.Functor.FullyFaithful
a57ac3a 
* master:
  chore: parallelize testing in CI (#845)
  feat: Match mathlib#17801 (#839)
  feat: Match mathlib#16761 (#840)
  feat: port CategoryTheory.NatIso (#820)
  feat: port algebra.ring.basic (#830)
  feat: port Combinatorics.Quiver.ConnectedComponent (#836)
  chore: bump to nightly-2022-12-03 (#838)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@YaelDillies @kim-em @Ruben-VandeVelde