精益證明助理中的交換環的冪等問題

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 

所以精益似乎已經忘記，是一個環？

因此，舉例來說，如果我改變了定義

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

那麼一切都很好。但這意味着我必須攜帶額外的簿記數據。有沒有辦法使用變量來解決保持簿記的需要。

Answer 1

默認情況下，Lean僅在實際使用它們的定義中包含節變量和參數。您可以使用include和omit命令覆蓋它。但由於comm_ring是一種類，你可能會想反正它聲明爲一類推理參數：

variables (A : Type) [comm_ring A] 

離開了參數的名稱一樣，這將包括在默認情況下，每一個定義，所以用你的定義應該起作用。