Yuyang Zhao 赵雨扬
Yuyang Zhao 赵雨扬
> > > 为什么要改成用命令来打开环境变量设置，感觉挺麻烦的。可以考虑用外部链接来解释如何打开修改环境变量的界面，或者恢复原先用图形界面打开的版本 > > > > > > 因为不同版本的 Windows 10 打开环境变量设置页面的步骤不尽相同，使用命令打开会更通用一些。 > > 我以前甚至没听说过能用 Win+R 运行 + 命令直接打开环境变量界面。 主要是感觉 “打开环境变量设置界面” 是一个一般化的需求，特别是考虑到 OI Wiki 中存在复数个页面提到这一设置： > > ...
I have just noticed something similar. In `Data.Nat.Properties` ```agda ≤-stepsˡ : ∀ {m n} o → m ≤ n → m ≤ o + n ≤-stepsʳ : ∀ {m n}...
> Actually, I am now trying out to remove duplicate lemmas from `algebra.order.ring` and i think that the guiding principle should be that the order of explicit assumptions in this...
Many of the lemmas in `zero_lt` still have stronger assumptions at the moment, mainly because `zero_le_one_class` and `zero_lt_one_class` (which is not even in the mathlib yet) are not used in...
I agree with this approach. On the other hand, I'm a bit worried that the lemmas in `zero_lt` are not fully completed and it may be too early to export...
I will change this PR to move the positivity assumption to the last, it seems better.
cls是clear screen
awaiting-review
I'm not sure where these diffs are. It might just be some mess from the merge.
> What's the status of this PR in respect to #366? In that PR we got: > > ``` > /-- > An induction principal that works on divison by...