린 증명 어시스턴트의 commutatitive 링 멱등호

Question

안녕하세요 저는 약식 어시스턴트에서 어떻게 작동하는지 알아보기 위해 수학을 시도하고 있습니다. 나는 환성 반지의 멱등 원 (idempotents of commutative ring)을 가지고 노는 것이 재미 있어야한다고 결정했다. 여기에 내가 시도 내용은 다음과 같습니다

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 

그래서 린 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] 

가와 있도록 매개 변수의 이름을 떠나는 당신의 정의가 효과가있다.