Hi I am trying to do some mathematics in the Lean proof assistant to see how it works. I decided that it should be fun to play with idempotents of a commutative ring. Here's what I tried:
variables (A : Type) (R : comm_ring A)
definition KR : Type := \Sigma x : A, x * x = x
I then get the error
failed to synthesize placeholder
A : Type,
x : A
⊢ has_mul A
So Lean seems to have forgotten that A is a ring?
So for example, if I change the definition to
definition KR (A : Type) (R : comm_ring A) : Type := Σ x : A , x = x * x
then everything is fine. But this means that I have to carry extra bookkeeping data. Is there a way to use variables to get around the need to keep bookkeeping stuff around.
By default, Lean includes section variables and parameters only in definitions that actually use them. You can override this with the include and omit commands. But since comm_ring is a type class, you'll likely want to declare it as a class inference parameter anyway:
variables (A : Type) [comm_ring A]
Leaving out the parameter's name like this will include it in every definition by default, so with that your definition should work.