How to use ring_hom.to_algebra

Stream: new members

[Amelia Livingston]

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]

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

[Reid Barton]

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

[Amelia Livingston]

Awesome, thank you