search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
15 stars 5 forks source link

field_simp は順序を扱えない #430

Closed Seasawher closed 5 days ago

Seasawher commented 5 days ago

実数上で

xy ≦ (x^2 + y^2)/2 に対して使用して上手くいかなかった（なぜ？）

Seasawher commented 5 days ago

Zulip: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/field_simp.20made.20no.20progress/near/448825044

Seasawher commented 5 days ago

そもそも体に順序があるとは限らないので、これはfield_simp の扱う範囲を超えている