## Stream: new members

### Topic: How to use ring_hom.to_algebra

#### Amelia Livingston (May 11 2020 at 22:15):

I must've missed something because this works here, but I can't work out what. I've tried changing the instance priority and the class.instance_max_depth.

import ring_theory.algebra

variables {R : Type*} {S : Type*}
(r : R) (s : S) [comm_semiring R] [comm_semiring S] (f : R →+* S)

instance foo : algebra R S := f.to_algebra

#check r • s -- failed to synthesize type class instance for has_scalar R S


#### Reid Barton (May 11 2020 at 22:28):

foo depends on f, but there's no way to infer it

#### Reid Barton (May 11 2020 at 22:29):

Whereas in the example you linked to, there's no extra variable

#### Amelia Livingston (May 11 2020 at 22:33):

Awesome, thank you

Last updated: May 10 2021 at 17:39 UTC