feat: port Data.Int.Cast.Lemmas (#995)

fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Dec 14, 2022 · 5c6a9da · 5c6a9da
1 parent 3db783c
commit 5c6a9da
Show file tree

Hide file tree

Showing 6 changed files with 449 additions and 33 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -157,9 +157,9 @@ import Mathlib.Data.FunLike.Embedding
 import Mathlib.Data.FunLike.Equiv
 import Mathlib.Data.HashMap
 import Mathlib.Data.Int.Basic
-import Mathlib.Data.Int.Cast
 import Mathlib.Data.Int.Cast.Basic
 import Mathlib.Data.Int.Cast.Defs
+import Mathlib.Data.Int.Cast.Lemmas
 import Mathlib.Data.Int.Dvd.Basic
 import Mathlib.Data.Int.LeastGreatest
 import Mathlib.Data.Int.Order.Basic

diff --git a/Mathlib/Algebra/GroupPower/Lemmas.lean b/Mathlib/Algebra/GroupPower/Lemmas.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import Mathlib.Data.Nat.Cast.Basic
-import Mathlib.Data.Int.Cast
+import Mathlib.Data.Int.Cast.Lemmas
 import Mathlib.Algebra.GroupPower.Basic
 
 /-!

diff --git a/Mathlib/Data/Int/Cast.lean b/Mathlib/Data/Int/Cast.lean
diff --git a/Mathlib/Data/Int/Cast/Basic.lean b/Mathlib/Data/Int/Cast/Basic.lean
@@ -10,7 +10,7 @@ import Mathlib.Algebra.Group.Basic
 # Cast of integers (additional theorems)
 
 This file proves additional properties about the *canonical* homomorphism from
-the integers into an additive group with a one (`int.cast`).
+the integers into an additive group with a one (`Int.cast`).
 
 There is also `Data.Int.Cast.Lemmas`,
 which includes lemmas stated in terms of algebraic homomorphisms,