search

leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 46 forks source link

Adding import algebra.group_power to exercise 4.6.4 #113

Open melembroucarlitos opened 3 years ago

melembroucarlitos commented 3 years ago

nat.pow was removed from core about a year ago, and it is necessary to complete this exercise