Commit 2021-12-17 15:21 c9fe6d1a

View on Github →

feat(algebra/algebra): instantiate ring_hom_class for alg_hom (#10853) This PR provides a ring_hom_class instance for alg_hom, to be used in #10783. I'm not quite finished with my design of morphism classes for linear maps, but I expect this instance will stick around anyway: to avoid a dangerous instance alg_hom_class F R A B → ring_hom_class F A B (where the base ring R can't be inferred), alg_hom_class will probably have to be unbundled and take a ring_hom_class as a parameter.

Estimated changes

Modified src/algebra/algebra/basic.lean

modified theorem alg_hom.coe_fn_inj

modified theorem alg_hom.coe_fn_injective

modified theorem alg_hom.coe_to_add_monoid_hom

modified theorem alg_hom.coe_to_monoid_hom

modified theorem alg_hom.ext

modified theorem alg_hom.ext_iff

modified theorem alg_hom.map_add

modified theorem alg_hom.map_bit0

modified theorem alg_hom.map_bit1

modified theorem alg_hom.map_mul

modified theorem alg_hom.map_neg

modified theorem alg_hom.map_one

modified theorem alg_hom.map_pow

modified theorem alg_hom.map_sub

modified theorem alg_hom.map_zero