max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add failing grind test about exponents (#9611)

Browse source
This commit is contained in:
Kim Morrison 2025-07-29 12:53:43 +10:00 • committed by GitHub
parent 969136b0d6
commit edade0cea8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/lean/grind/algebra/exponents.lean
View file

@ -13,6 +13,11 @@ example (n m : Nat) : (n+m)^2 = n^2 + 2*n*m + m^2 := by grind
example (a : R) (n m : Nat) : a^((n+m)^2) = a^(n^2 + 2*n*m + m^2) := by grind
example (a : R) (n m : Nat) : a^((n+m)^2) = a^(n^2) * a^(2*n*m) * a^(m^2) := by grind
-- from Mathlib.NumberTheory.Multiplicity
theorem pow_two_pow_sub_pow_two_pow.extracted_1_1 {x y : R} (d : Nat) :
x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d) := by
grind
end CommRing