proof - 精益证明助手中交换环的幂等性

Question

嗨，我正在尝试在精益证明助手中做一些数学运算，看看它是如何工作的。我认为与交换环的幂等一起玩应该很有趣。这是我尝试过的：

variables (A : Type) (R : comm_ring A)
definition KR : Type := \Sigma x : A, x * x = x

然后我得到错误

failed to synthesize placeholder
A : Type,
x : A
⊢ has_mul A

所以 Lean 似乎忘记了 A 是一个环？

例如，如果我将定义更改为

definition KR (A : Type) (R : comm_ring A) :  Type := Σ x : A , x = x * x

那么一切都很好。但这意味着我必须携带额外的簿记数据。有没有办法使用变量来解决保留簿记的需要。

Answer 1

默认情况下，Lean 仅在实际使用它们的定义中包含部分变量和参数。您可以使用includeandomit命令覆盖它。但由于comm_ring它是一个类型类，您可能还是希望将其声明为类推理参数：

variables (A : Type) [comm_ring A]

像这样省略参数的名称将默认将其包含在每个定义中，因此您的定义应该可以工作。