【Lean4】ring

ring

可換環における多項式恒等式を証明する

example (x y : ℤ) :
    (x + y)^2 = x^2 + 2*x*y + y^2 := by
  ring

example (x y : ℤ) :
    (x + y)^2 = x^2 + 2*x*y + y^2 := by
  ring

式を展開・整理すれば等しいタイプの証明に使う