>有限次元の線形空間を Leanで扱えるようにはなっても
>当然だが、無限次元は扱えない

こんなあんぽんたんなこと平気でいっててつっかかってくる無能はなんなんや