algebra maps takes 1 to 1

Stream: new members

[Vasily Ilin]

Why am I getting an error here?

import ring_theory.tensor_product
import tactic

universe u
variables (K : Type u) [comm_semiring K] (A : Type u) [semiring A] [algebra K A]
variable (f : A →ₐ A) -- ERROR: don't know how to synthesize placeholder

[Damiano Testa]

I'm on mobile and the symbols are mangled, but can K be inferred there?

[Damiano Testa]

E.g., how does lean know whether K is ℕ or not?

[Vasily Ilin]

yup, that's totally it! Thank you