Идемпотенты коммутативного кольца в помощнике по проверке на лету

Question

Привет, я пытаюсь сделать некоторую математику в помощнике Lean proof, чтобы посмотреть, как это работает. Я решил, что должно быть весело играть с идемпотентами коммутативного кольца. Вот что я пробовал:

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, кажется, забыли, что А кольцо?

Так, например, если изменить определение

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] 

Опуская имя параметра, как это будет включать его в каждом определении по умолчанию, так что с этим вашим определение должно работать.