mathlib3
aab0b2df - feat(algebra/algebra/basic): add some lemmas about `subsemiring` and `algebra_map` (#13767)

Commit
3 years ago
feat(algebra/algebra/basic): add some lemmas about `subsemiring` and `algebra_map` (#13767) These are analogs of `algebra_map_of_subring`, `coe_algebra_map_of_subring` and `algebra_map_of_subring_apply`.
Author
Parents
Loading