9d57ed83a9
This PR upstreams many of the results from `Mathlib/Data/Int/Init.lean`. Notably, we upstream the `simp` tag on `Int.natCast_pow`. While this is desirable as a `simp` lemma, it is non-confluent with other good `simp` lemmas like `Int.emod_bmod_congr`, and this will need to be addressed in the future. |
||
|---|---|---|
| .. | ||
| Basic.lean | ||
| Bootstrap.lean | ||
| Lemmas.lean | ||