Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+β Ctrl+β to navigate,
Ctrl+π±οΈ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Gabriel Ebner
! This file was ported from Lean 3 source module data.int.cast.basic
! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Int.Cast.Defs
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`).
There is also `Data.Int.Cast.Lemmas`,
which includes lemmas stated in terms of algebraic homomorphisms,
and results involving the order structure of `β€`.
By contrast, this file's only import beyond `Data.Int.Cast.Defs` is `Algebra.Group.Basic`.
-/
universe u
namespace Nat
variable { R : Type u } [ AddGroupWithOne : Type ?u.4 β Type ?u.4 R ]
@[ simp , norm_cast ]
theorem cast_sub { m n } ( h : m β€ n ) : (( n - m : β ) : R ) = n - m :=
eq_sub_of_add_eq : β {G : Type ?u.329} [inst : AddGroup G a b c : G }, a + c = b a = b - c <| by rw [ β cast_add , Nat.sub_add_cancel : β {n m : β }, m β€ n n - m + m = n h ]
#align nat.cast_sub Nat.cast_subβ
-- `HasLiftT` appeared in the type signature
@[ simp , norm_cast ]
theorem cast_pred : β {n : β }, 0 < n β(n - 1 = βn - 1 cast_pred : β { n }, 0 < n β (( n - 1 : β ) : R ) = n - 1
| 0 , h => by cases h
| n + 1, _ => by β(n + 1 - 1 = β(n + 1 - 1 rw [ β(n + 1 - 1 = β(n + 1 - 1 cast_succ , β(n + 1 - 1 = βn + 1 - 1 β(n + 1 - 1 = β(n + 1 - 1 add_sub_cancel : β {G : Type ?u.1216} [inst : AddGroup G a b : G ), a + b - b = a ] ; β(n + 1 - 1 = β(n + 1 - 1 rfl
#align nat.cast_pred Nat.cast_pred
end Nat
open Nat
namespace Int
variable { R : Type u } [ AddGroupWithOne : Type ?u.4816 β Type ?u.4816 R ]
@[ simp , norm_cast ]
theorem cast_negSucc ( n : β ) : (-[ n +1] : R ) = -( n + 1 : β ) :=
AddGroupWithOne.intCast_negSucc n
#align int.cast_neg_succ_of_nat Int.cast_negSuccβ
-- expected `n` to be implicit, and `HasLiftT`
@[ simp , norm_cast ]
theorem cast_zero : (( 0 : β€ ) : R ) = 0 :=
( AddGroupWithOne.intCast_ofNat 0 ). trans : β {Ξ± : Sort ?u.1967} {a b c : Ξ± }, a = b b = c a = c trans Nat.cast_zero
#align int.cast_zero Int.cast_zeroβ
-- type had `HasLiftT`
@[ simp high , nolint simpNF , norm_cast ] -- this lemma competes with `Int.ofNat_eq_cast` to come later
theorem cast_ofNat ( n : β ) : (( n : β€ ) : R ) = n :=
AddGroupWithOne.intCast_ofNat _
#align int.cast_coe_nat Int.cast_ofNatβ
-- expected `n` to be implicit, and `HasLiftT`
#align int.cast_of_nat Int.cast_ofNatβ
@[ simp , norm_cast ]
theorem int_cast_ofNat ( n : β ) [ n . AtLeastTwo ] :
(( OfNat.ofNat : {Ξ± : Type ?u.2325} β (x : β ) β [self : OfNat Ξ± x Ξ± n : β€ ) : R ) = OfNat.ofNat : {Ξ± : Type ?u.2379} β (x : β ) β [self : OfNat Ξ± x Ξ± n := by
simpa only [ OfNat.ofNat : {Ξ± : Type ?u.2436} β (x : β ) β [self : OfNat Ξ± x Ξ± ] using AddGroupWithOne.intCast_ofNat (R := R ) n
@[ simp , norm_cast ]
theorem cast_one : (( 1 : β€ ) : R ) = 1 := by
erw [ cast_ofNat , Nat.cast_one ]
#align int.cast_one Int.cast_oneβ
-- type had `HasLiftT`
@[ simp , norm_cast ]
theorem cast_neg : β (n : β€ ), β(- n = - βn cast_neg : β n , ((- n : β€ ) : R ) = - n
| (0 : β) => by erw [ cast_zero , neg_zero ]
| ( n + 1 : β) => by β(- β(n + 1 = - ββ(n + 1 erw [ β(- β(n + 1 = - ββ(n + 1 cast_ofNat , β(- β(n + 1 = - β(n + 1 β(- β(n + 1 = - ββ(n + 1 cast_negSucc ]
| -[ n +1] => by erw [ cast_ofNat , cast_negSucc , neg_neg ]
#align int.cast_neg Int.cast_negβ
-- type had `HasLiftT`
@[ simp , norm_cast ]
theorem cast_subNatNat ( m n ) : (( Int.subNatNat m n : β€ ) : R ) = m - n := by
unfold subNatNat
cases e : n - m
Β· simp only [ ofNat_eq_coe ] zero ββ(m - n = βm - βn
simp [ e , Nat.le_of_sub_eq_zero : β {n m : β }, n - m = 0 n β€ m e ]
Β· rw [ cast_negSucc , succ - β(nβ + 1 = βm - βn Nat.add_one , β e , succ - β(n - m = βm - βn Nat.cast_sub <| _root_.le_of_lt : β {Ξ± : Type ?u.4548} [inst : Preorder Ξ± a b : Ξ± }, a < b a β€ b <| Nat.lt_of_sub_eq_succ : β {m n l : β }, m - n = succ l n < m e , succ - (βn - βm = βm - βn
neg_sub succ βm - βn = βm - βn ]
#align int.cast_sub_nat_nat Int.cast_subNatNatβ
-- type had `HasLiftT`
#align int.neg_of_nat_eq Int.negOfNat_eq
@[ simp ]
theorem cast_negOfNat ( n : β ) : (( negOfNat n : β€ ) : R ) = - n := by simp [ Int.cast_neg , negOfNat_eq ]
#align int.cast_neg_of_nat Int.cast_negOfNat
@[ simp , norm_cast ]
theorem cast_add : β m n , (( m + n : β€ ) : R ) = m + n
| (m : β), (n : β) => by β(βm + βn = ββm + ββn simp [β Int.ofNat_add : β (n m : β ), β(n + m = βn + βm , Nat.cast_add ]
| (m : β), -[ n +1] => by erw [ cast_subNatNat , cast_ofNat , cast_negSucc , sub_eq_add_neg ]
| -[ m +1], (n : β) => by
erw [ cast_subNatNat , cast_ofNat , cast_negSucc , sub_eq_iff_eq_add : β {G : Type ?u.7599} [inst : AddGroup G a b c : G }, a - b = c β a = c + b , add_assoc ,
eq_neg_add_iff_add_eq : β {G : Type ?u.7729} [inst : AddGroup G a b c : G }, a = - b + c β b + a = c , β Nat.cast_add , β Nat.cast_add , Nat.add_comm : β (n m : β ), n + m = m + n ]
| -[ m +1], -[ n +1] =>
show (-[ m + n + 1 +1] : R ) = _ by
rw [ cast_negSucc , cast_negSucc , cast_negSucc , β neg_add_rev , - β(m + n + 1 + 1 = - (β(n + 1 + β(m + 1 β Nat.cast_add ,
Nat.add_right_comm : β (n m k : β ), n + m + k = n + k + m m n 1 , Nat.add_assoc : β (n m k : β ), n + m + k = n + (m + k , - β(m + 1 + (n + 1 = - β(n + 1 + (m + 1 Nat.add_comm : β (n m : β ), n + m = m + n - β(n + 1 + (m + 1 = - β(n + 1 + (m + 1 ]
#align int.cast_add Int.cast_addβ
-- type had `HasLiftT`
@[ simp , norm_cast ]
theorem cast_sub : β (m n : β€ ), β(m - n = βm - βn cast_sub ( m n ) : (( m - n : β€ ) : R ) = m - n := by
simp [ Int.sub_eq_add_neg : β {a b : β€ }, a - b = a + - b , sub_eq_add_neg , Int.cast_neg , Int.cast_add ]
#align int.cast_sub Int.cast_subβ
-- type had `HasLiftT`
section deprecated
set_option linter.deprecated false
@[ norm_cast , deprecated ]
theorem ofNat_bit0 ( n : β ) : (β( bit0 : {Ξ± : Type ?u.9688} β [inst : Add Ξ± Ξ± β Ξ± n ) : β€ ) = bit0 : {Ξ± : Type ?u.9731} β [inst : Add Ξ± Ξ± β Ξ± β n :=
rfl : β {Ξ± : Sort ?u.9775} {a : Ξ± }, a = a
#align int.coe_nat_bit0 Int.ofNat_bit0
@[ norm_cast , deprecated ]
theorem ofNat_bit1 ( n : β ) : (β( bit1 : {Ξ± : Type ?u.9849} β [inst : One Ξ± [inst : Add Ξ± Ξ± β Ξ± n ) : β€ ) = bit1 : {Ξ± : Type ?u.10040} β [inst : One Ξ± [inst : Add Ξ± Ξ± β Ξ± β n :=
rfl : β {Ξ± : Sort ?u.10234} {a : Ξ± }, a = a
#align int.coe_nat_bit1 Int.ofNat_bit1
@[ norm_cast , deprecated ]
theorem cast_bit0 ( n : β€ ) : (( bit0 : {Ξ± : Type ?u.10325} β [inst : Add Ξ± Ξ± β Ξ± n : β€ ) : R ) = bit0 : {Ξ± : Type ?u.10380} β [inst : Add Ξ± Ξ± β Ξ± ( n : R ) :=
Int.cast_add _ _
#align int.cast_bit0 Int.cast_bit0
@[ norm_cast , deprecated ]
theorem cast_bit1 ( n : β€ ) : (( bit1 : {Ξ± : Type ?u.10540} β [inst : One Ξ± [inst : Add Ξ± Ξ± β Ξ± n : β€ ) : R ) = bit1 : {Ξ± : Type ?u.10765} β [inst : One Ξ± [inst : Add Ξ± Ξ± β Ξ± ( n : R ) :=
by rw [ bit1 : {Ξ± : Type ?u.11078} β [inst : One Ξ± [inst : Add Ξ± Ξ± β Ξ± , Int.cast_add , Int.cast_one , cast_bit0 ] ; rfl
#align int.cast_bit1 Int.cast_bit1
end deprecated
theorem cast_two : (( 2 : β€ ) : R ) = 2 :=
show ((( 2 : β ) : β€ ) : R ) = (( 2 : β ) : R ) by rw [ cast_ofNat , Nat.cast_ofNat ]
#align int.cast_two Int.cast_two
theorem cast_three : (( 3 : β€ ) : R ) = 3 :=
show ((( 3 : β ) : β€ ) : R ) = (( 3 : β ) : R ) by rw [ cast_ofNat , Nat.cast_ofNat ]
#align int.cast_three Int.cast_three
theorem cast_four : (( 4 : β€ ) : R ) = 4 :=
show ((( 4 : β ) : β€ ) : R ) = (( 4 : β ) : R ) by rw [ cast_ofNat , Nat.cast_ofNat ]
#align int.cast_four Int.cast_four
end Int