[Merged by Bors] - fix(algebra/monoid_algebra/basic): add int_cast to monoid_algebra instances
#15779
Conversation
ericrbg
added
awaiting-CI
mathlib-dependent-issues-bot
added
the
blocked-by-other-PR
github-actions
bot
removed
the
awaiting-CI
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
| @@of_irreducible_map _ _ _ (is_local_ring_hom_expand R hp.bot_lt) hf | ||
| let _ := is_local_ring_hom_expand R hp.bot_lt in by exactI of_irreducible_map ↑(expand R p) hf |
There was a problem hiding this comment.
Any idea what happened here?
There was a problem hiding this comment.
not really sure, but the typechecking has been crazy brittle with int_cast and stuff: for some further examples that bewilder me, look at this and its fix [and no, deinstancing the comm_semiring instance didn't help at all]
e: the error isn't obvious, it's https://github.com/leanprover-community/mathlib/runs/7601089733?check_suite_focus=true and the only way I managed to fix it without just undoing my changes was by using refine like 5 times to define that function (and the equivalent version for mv_polynomial further down the file)
There was a problem hiding this comment.
Either way, I guess this is nicer because it avoids an @
| @@ -173,6 +173,9 @@ rfl | |||
| /-- `polynomial.algebra_of_algebra` is consistent with `algebra_nat`. -/ | |||
| example [comm_semiring R] : (polynomial.algebra_of_algebra : algebra ℕ R[X]) = algebra_nat := rfl | |||
|
|
|||
| /-- `polynomial.algebra_of_algebra` is consistent with `algebra_int`. -/ | |||
| example [ring R] : (polynomial.algebra_of_algebra : algebra ℤ R[X]) = algebra_int _ := rfl | |||
There was a problem hiding this comment.
I guess the line above only needs semiring R then, my mistake.
|
✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
|
bors r+ |
… instances (#15779) Note that this reshuffles how some instances are created to ensure that they get the `int_cast` field. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
int_cast to monoid_algebra instancesint_cast to monoid_algebra instances
… instances (#15779) Note that this reshuffles how some instances are created to ensure that they get the `int_cast` field. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
… instances (#15779) Note that this reshuffles how some instances are created to ensure that they get the `int_cast` field. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Note that this reshuffles how some instances are created to ensure that they get the
int_castfield.monomial_funto remove diamonds #15778