Zulip Chat Archive

Stream: new members

Topic: algebra maps takes 1 to 1


Vasily Ilin (Apr 20 2022 at 19:53):

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 (Apr 20 2022 at 19:57):

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

Damiano Testa (Apr 20 2022 at 19:58):

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

Vasily Ilin (Apr 20 2022 at 19:59):

yup, that's totally it! Thank you


Last updated: Dec 20 2023 at 11:08 UTC