Leanに詳しい人教えて、mathlibにエタールコホモロジーが入ってないのはなんで？

Leanに詳しい人教えて、mathlibにエタールコホモロジーが入ってないのはなんで？ (3ﾚｽ)
上下前次 1-新

1(2): 05/01(木)13:53 ID:WPE4OMis(1) AAS
Perfectoid spaceを形式化するよりよっぽど簡単だと思うんだがどこで詰まってるの？
GPTに聞いたらスキームですらまともに扱えてないとか言ってんだけど

2: 05/01(木)15:39 ID:joN5psCP(1) AAS
>>1
くだらないスレを立てるな
どうしてもくだらないスレを立てたいなら、せめてくだらない話題で立てろ