ring): add new `int_cast` and `nat_cast` fields to match `ring` and `semiring` (#14976)

Commit

3 years ago

chore(algebra/direct_sum/ring): add new `int_cast` and `nat_cast` fields to match `ring` and `semiring` (#14976) This was deliberately left to a follow up in #12182

Author

eric-wieser

Parents

af8ca85d

mathlib3 671c7c05 - chore(algebra/direct_sum/ring): add new `int_cast` and `nat_cast` fields to match `ring` and `semiring` (#14976)

mathlib3
671c7c05 - chore(algebra/direct_sum/ring): add new `int_cast` and `nat_cast` fields to match `ring` and `semiring` (#14976)