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

默认情况下，精益仅在实际使用它们的定义中包含部分变量和参数。您可以使用 include 和 omit 命令覆盖它。但是由于 comm_ring 是一个类型类，您可能无论如何都希望将其声明为类推理参数:

variables (A : Type) [comm_ring A]

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