[Merged by Bors] - chore(SetTheory/Cardinal/Basic): inline mul_comm into instance
#16851
Conversation
PR summary dd08cb466aImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for |
| inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumArrowEquivProdArrow β γ α | ||
|
|
||
| private theorem cast_succ (n : ℕ) : ((n + 1 : ℕ) : Cardinal.{u}) = n + 1 := by | ||
| change #(ULift.{u} _) = #(ULift.{u} _) + 1 |
There was a problem hiding this comment.
Out of scope if you want it to be, but it would be nice to have a natCast_def lemma that avoids the need for this change.
There was a problem hiding this comment.
This wouldn't be very useful, as it'd be essentially subsumed by Cardinal.mk_fintype.
There was a problem hiding this comment.
The same could be said for add_def vs mk_sum though, right?
There was a problem hiding this comment.
Not quite, since one is universe polymorphic, while the other is more convenient in the case the universes are equal.
#(Ulift (Fin n)) = n is just rw [Cardinal.mk_ulift, Cardinal.mk_fintype, Fintype.card_fin], and it's not like it adds a lot of convenience (under what other context are you going to be using Ulift (Fin n)?).
There was a problem hiding this comment.
In fact, we should probably redefine ↑n as the def-eq lift #(Fin n). Then I think it would make more sense to have natCast_def.
There was a problem hiding this comment.
theorem Cardinal.natCast_def (n : ℕ) : (n : Cardinal.{u}) = #(ULift.{u} (Fin n)) := by
rw [mk_uLift, mk_fin, lift_natCast]is probably the steps you're thinking of; but I think I'd still argue that the lemma is worth having since it's rfl and avoids a change. No need to pull this PR back from bors though.
|
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
mul_comm into instancemul_comm into instance
We also make the arguments of
power_zero,power_one, andpower_addexplicit.