Closed Seasawher closed 7 months ago
https://aconite-ac.github.io/theorem_proving_in_lean4_ja/tactics.html#using-the-simplifier-%E5%8D%98%E7%B4%94%E5%8C%96%E5%99%A8%E3%81%AE%E4%BD%BF%E7%94%A8
自然数の乗法のような可換性と結合性を満たす演算の場合、単純化器は可換性と結合性に加えてleft commutativity(左結合性)を用いて式を書き換える。乗法の場合、左結合性は次のように表される
左結合性ではなくて左可換性です.
ご指摘ありがとうございます。 明らかな誤訳ですので修正いたします。 当該段落で同様の誤りが複数ありましたので、一括修正いたします。
https://aconite-ac.github.io/theorem_proving_in_lean4_ja/tactics.html#using-the-simplifier-%E5%8D%98%E7%B4%94%E5%8C%96%E5%99%A8%E3%81%AE%E4%BD%BF%E7%94%A8
左結合性ではなくて左可換性です.