Tous les labs

Polynomial normalization

2/4 ~10 minlean

Prove the difference-of-squares identity over integers.

4 lines · Lean 4
Vérifier dans Lean Web
Objectifs
  • Prove the difference-of-squares identity over integers.
Indices
Voir la solution
import Mathlib

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