@@ -137,12 +137,12 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
| ofNat _ = > show ofNat _ = _ by simp
| - [ _ + 1 ] = > rfl
@[ simp ] protected theorem zero_div : ∀ b : Int , div 0 b = 0
@[ simp ] protected theorem zero_t div : ∀ b : Int , t div 0 b = 0
| ofNat _ = > show ofNat _ = _ by simp
| - [ _ + 1 ] = > show - ofNat _ = _ by simp
unseal Nat . div in
@[ simp ] protected theorem div_zero : ∀ a : Int , div a 0 = 0
@[ simp ] protected theorem t div_zero : ∀ a : Int , t div a 0 = 0
| ofNat _ = > show ofNat _ = _ by simp
| - [ _ + 1 ] = > rfl
@@ -156,16 +156,17 @@ unseal Nat.div in
/- ! ### div equivalences -/
theorem div_eq_ediv : ∀ { a b : Int } , 0 ≤ a → 0 ≤ b → a . div b = a / b
theorem t div_eq_ediv : ∀ { a b : Int } , 0 ≤ a → 0 ≤ b → a . t div b = a / b
| 0 , _ , _ , _ | _ , 0 , _ , _ = > by simp
| succ _ , succ _ , _ , _ = > rfl
theorem fdiv_eq_ediv : ∀ ( a : Int ) { b : Int } , 0 ≤ b → fdiv a b = a / b
| 0 , _ , _ | - [ _ + 1 ] , 0 , _ = > by simp
| succ _ , ofNat _ , _ | - [ _ + 1 ] , succ _ , _ = > rfl
theorem fdiv_eq_div { a b : Int } ( Ha : 0 ≤ a ) ( Hb : 0 ≤ b ) : fdiv a b = div a b : =
div_eq_ediv Ha Hb ▸ fdiv_eq_ediv _ Hb
theorem fdiv_eq_t div { a b : Int } ( Ha : 0 ≤ a ) ( Hb : 0 ≤ b ) : fdiv a b = t div a b : =
t div_eq_ediv Ha Hb ▸ fdiv_eq_ediv _ Hb
/- ! ### mod zero -/
@@ -175,9 +176,9 @@ theorem fdiv_eq_div {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = div a
| ofNat _ = > congrArg ofNat < | Nat . mod_zero _
| - [ _ + 1 ] = > congrArg negSucc < | Nat . mod_zero _
@[ simp ] theorem zero_mod ( b : Int ) : mod 0 b = 0 : = by cases b < ; > simp [ mod ]
@[ simp ] theorem zero_t mod ( b : Int ) : t mod 0 b = 0 : = by cases b < ; > simp [ t mod]
@[ simp ] theorem mod_zero : ∀ a : Int , mod a 0 = a
@[ simp ] theorem t mod_zero : ∀ a : Int , t mod a 0 = a
| ofNat _ = > congrArg ofNat < | Nat . mod_zero _
| - [ _ + 1 ] = > congrArg ( fun n = > - ofNat n ) < | Nat . mod_zero _
@@ -221,7 +222,7 @@ theorem ediv_add_emod' (a b : Int) : a / b * b + a % b = a := by
theorem emod_def ( a b : Int ) : a % b = a - b * ( a / b ) : = by
rw [ ← Int . add_sub_cancel ( a % b ) , emod_add_ediv ]
theorem mod_add_div : ∀ a b : Int , mod a b + b * ( a . div b ) = a
theorem t mod_add_t div : ∀ a b : Int , t mod a b + b * ( a . t div b ) = a
| ofNat _ , ofNat _ = > congrArg ofNat ( Nat . mod_add_div . . )
| ofNat m , - [ n + 1 ] = > by
show ( m % succ n + - ↑ ( succ n ) * - ↑ ( m / succ n ) : Int ) = m
@@ -238,17 +239,17 @@ theorem mod_add_div : ∀ a b : Int, mod a b + b * (a.div b) = a
rw [ Int . neg_mul , ← Int . neg_add ]
exact congrArg ( - ofNat · ) ( Nat . mod_add_div . . )
theorem div_add_mod ( a b : Int ) : b * a . div b + mod a b = a : = by
rw [ Int . add_comm ] ; apply mod_add_div . .
theorem t div_add_t mod ( a b : Int ) : b * a . t div b + t mod a b = a : = by
rw [ Int . add_comm ] ; apply t mod_add_t div . .
theorem mod_add_div' ( m k : Int ) : mod m k + m . div k * k = m : = by
rw [ Int . mul_comm ] ; apply mod_add_div
theorem t mod_add_t div' ( m k : Int ) : t mod m k + m . t div k * k = m : = by
rw [ Int . mul_comm ] ; apply t mod_add_t div
theorem div_add_mod' ( m k : Int ) : m . div k * k + mod m k = m : = by
rw [ Int . mul_comm ] ; apply div_add_mod
theorem t div_add_t mod' ( m k : Int ) : m . t div k * k + t mod m k = m : = by
rw [ Int . mul_comm ] ; apply t div_add_t mod
theorem mod_def ( a b : Int ) : mod a b = a - b * a . div b : = by
rw [ ← Int . add_sub_cancel ( mod a b ) , mod_add_div ]
theorem t mod_def ( a b : Int ) : t mod a b = a - b * a . t div b : = by
rw [ ← Int . add_sub_cancel ( t mod a b ) , t mod_add_t div]
theorem fmod_add_fdiv : ∀ a b : Int , a . fmod b + b * a . fdiv b = a
| 0 , ofNat _ | 0 , - [ _ + 1 ] = > congrArg ofNat < | by simp
@@ -278,11 +279,11 @@ theorem fmod_def (a b : Int) : a.fmod b = a - b * a.fdiv b := by
theorem fmod_eq_emod ( a : Int ) { b : Int } ( hb : 0 ≤ b ) : fmod a b = a % b : = by
simp [ fmod_def , emod_def , fdiv_eq_ediv _ hb ]
theorem mod_eq_emod { a b : Int } ( ha : 0 ≤ a ) ( hb : 0 ≤ b ) : mod a b = a % b : = by
simp [ emod_def , mod_def , div_eq_ediv ha hb ]
theorem t mod_eq_emod { a b : Int } ( ha : 0 ≤ a ) ( hb : 0 ≤ b ) : t mod a b = a % b : = by
simp [ emod_def , t mod_def, t div_eq_ediv ha hb ]
theorem fmod_eq_mod { a b : Int } ( Ha : 0 ≤ a ) ( Hb : 0 ≤ b ) : fmod a b = mod a b : =
mod_eq_emod Ha Hb ▸ fmod_eq_emod _ Hb
theorem fmod_eq_t mod { a b : Int } ( Ha : 0 ≤ a ) ( Hb : 0 ≤ b ) : fmod a b = t mod a b : =
t mod_eq_emod Ha Hb ▸ fmod_eq_emod _ Hb
/- ! ### ` / ` ediv -/
@@ -297,7 +298,7 @@ theorem ediv_neg' {a b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0 :=
protected theorem div_def ( a b : Int ) : a / b = Int . ediv a b : = rfl
theorem negSucc_ediv ( m : Nat ) { b : Int } ( H : 0 < b ) : - [ m + 1 ] / b = - ( div m b + 1 ) : =
theorem negSucc_ediv ( m : Nat ) { b : Int } ( H : 0 < b ) : - [ m + 1 ] / b = - ( e div m b + 1 ) : =
match b , eq_succ_of_zero_lt H with
| _ , ⟨ _ , rfl ⟩ = > rfl
@@ -796,191 +797,191 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
Int . ediv_eq_of_eq_mul_right H3 < | by
rw [ ← Int . mul_ediv_assoc _ H2 ] ; exact ( Int . ediv_eq_of_eq_mul_left H4 H5 . symm ) . symm
/- ! ### div -/
/- ! ### t div -/
@[ simp ] protected theorem div_one : ∀ a : Int , a . div 1 = a
@[ simp ] protected theorem t div_one : ∀ a : Int , a . t div 1 = a
| ( n : Nat ) = > congrArg ofNat ( Nat . div_one _ )
| - [ n + 1 ] = > by simp [ Int . div , neg_ofNat_succ ] ; rfl
| - [ n + 1 ] = > by simp [ Int . t div, neg_ofNat_succ ] ; rfl
unseal Nat . div in
@[ simp ] protected theorem div_neg : ∀ a b : Int , a . div ( - b ) = - ( a . div b )
@[ simp ] protected theorem t div_neg : ∀ a b : Int , a . t div ( - b ) = - ( a . t div b )
| ofNat m , 0 = > show ofNat ( m / 0 ) = - ↑ ( m / 0 ) by rw [ Nat . div_zero ] ; rfl
| ofNat m , - [ n + 1 ] | - [ m + 1 ] , succ n = > ( Int . neg_neg _ ) . symm
| ofNat m , succ n | - [ m + 1 ] , 0 | - [ m + 1 ] , - [ n + 1 ] = > rfl
unseal Nat . div in
@[ simp ] protected theorem neg_div : ∀ a b : Int , ( - a ) . div b = - ( a . div b )
@[ simp ] protected theorem neg_t div : ∀ a b : Int , ( - a ) . t div b = - ( a . t div b )
| 0 , n = > by simp [ Int . neg_zero ]
| succ m , ( n : Nat ) | - [ m + 1 ] , 0 | - [ m + 1 ] , - [ n + 1 ] = > rfl
| succ m , - [ n + 1 ] | - [ m + 1 ] , succ n = > ( Int . neg_neg _ ) . symm
protected theorem neg_div_neg ( a b : Int ) : ( - a ) . div ( - b ) = a . div b : = by
simp [ Int . div_neg , Int . neg_div , Int . neg_neg ]
protected theorem neg_t div_neg ( a b : Int ) : ( - a ) . t div ( - b ) = a . t div b : = by
simp [ Int . t div_neg, Int . neg_t div , Int . neg_neg ]
protected theorem div_nonneg { a b : Int } ( Ha : 0 ≤ a ) ( Hb : 0 ≤ b ) : 0 ≤ a . div b : =
protected theorem t div_nonneg { a b : Int } ( Ha : 0 ≤ a ) ( Hb : 0 ≤ b ) : 0 ≤ a . t div b : =
match a , b , eq_ofNat_of_zero_le Ha , eq_ofNat_of_zero_le Hb with
| _ , _ , ⟨ _ , rfl ⟩ , ⟨ _ , rfl ⟩ = > ofNat_zero_le _
protected theorem div_nonpos { a b : Int } ( Ha : 0 ≤ a ) ( Hb : b ≤ 0 ) : a . div b ≤ 0 : =
Int . nonpos_of_neg_nonneg < | Int . div_neg . . ▸ Int . div_nonneg Ha ( Int . neg_nonneg_of_nonpos Hb )
protected theorem t div_nonpos { a b : Int } ( Ha : 0 ≤ a ) ( Hb : b ≤ 0 ) : a . t div b ≤ 0 : =
Int . nonpos_of_neg_nonneg < | Int . t div_neg . . ▸ Int . t div_nonneg Ha ( Int . neg_nonneg_of_nonpos Hb )
theorem div_eq_zero_of_lt { a b : Int } ( H1 : 0 ≤ a ) ( H2 : a < b ) : a . div b = 0 : =
theorem t div_eq_zero_of_lt { a b : Int } ( H1 : 0 ≤ a ) ( H2 : a < b ) : a . t div b = 0 : =
match a , b , eq_ofNat_of_zero_le H1 , eq_succ_of_zero_lt ( Int . lt_of_le_of_lt H1 H2 ) with
| _ , _ , ⟨ _ , rfl ⟩ , ⟨ _ , rfl ⟩ = > congrArg Nat . cast < | Nat . div_eq_of_lt < | ofNat_lt . 1 H2
@[ simp ] protected theorem mul_div_cancel ( a : Int ) { b : Int } ( H : b ≠ 0 ) : ( a * b ) . div b = a : =
have : ∀ { a b : Nat } , ( b : Int ) ≠ 0 → ( div ( a * b ) b : Int ) = a : = fun H = > by
rw [ ← ofNat_mul , ← ofNat_div ,
@[ simp ] protected theorem mul_t div_cancel ( a : Int ) { b : Int } ( H : b ≠ 0 ) : ( a * b ) . t div b = a : =
have : ∀ { a b : Nat } , ( b : Int ) ≠ 0 → ( t div ( a * b ) b : Int ) = a : = fun H = > by
rw [ ← ofNat_mul , ← ofNat_t div ,
Nat . mul_div_cancel _ < | Nat . pos_of_ne_zero < | Int . ofNat_ne_zero . 1 H ]
match a , b , a . eq_nat_or_neg , b . eq_nat_or_neg with
| _ , _ , ⟨ a , . inl rfl ⟩ , ⟨ b , . inl rfl ⟩ = > this H
| _ , _ , ⟨ a , . inl rfl ⟩ , ⟨ b , . inr rfl ⟩ = > by
rw [ Int . mul_neg , Int . neg_div , Int . div_neg , Int . neg_neg ,
rw [ Int . mul_neg , Int . neg_t div , Int . t div_neg, Int . neg_neg ,
this ( Int . neg_ne_zero . 1 H ) ]
| _ , _ , ⟨ a , . inr rfl ⟩ , ⟨ b , . inl rfl ⟩ = > by rw [ Int . neg_mul , Int . neg_div , this H ]
| _ , _ , ⟨ a , . inr rfl ⟩ , ⟨ b , . inl rfl ⟩ = > by rw [ Int . neg_mul , Int . neg_t div , this H ]
| _ , _ , ⟨ a , . inr rfl ⟩ , ⟨ b , . inr rfl ⟩ = > by
rw [ Int . neg_mul_neg , Int . div_neg , this ( Int . neg_ne_zero . 1 H ) ]
rw [ Int . neg_mul_neg , Int . t div_neg, this ( Int . neg_ne_zero . 1 H ) ]
@[ simp ] protected theorem mul_div_cancel_left ( b : Int ) ( H : a ≠ 0 ) : ( a * b ) . div a = b : =
Int . mul_comm . . ▸ Int . mul_div_cancel _ H
@[ simp ] protected theorem mul_t div_cancel_left ( b : Int ) ( H : a ≠ 0 ) : ( a * b ) . t div a = b : =
Int . mul_comm . . ▸ Int . mul_t div_cancel _ H
@[ simp ] protected theorem div_self { a : Int } ( H : a ≠ 0 ) : a . div a = 1 : = by
have : = Int . mul_div_cancel 1 H ; rwa [ Int . one_mul ] at this
@[ simp ] protected theorem t div_self { a : Int } ( H : a ≠ 0 ) : a . t div a = 1 : = by
have : = Int . mul_t div_cancel 1 H ; rwa [ Int . one_mul ] at this
theorem mul_div_cancel_of_mod_eq_zero { a b : Int } ( H : a . mod b = 0 ) : b * ( a . div b ) = a : = by
have : = mod_add_div a b ; rwa [ H , Int . zero_add ] at this
theorem mul_t div_cancel_of_t mod_eq_zero { a b : Int } ( H : a . t mod b = 0 ) : b * ( a . t div b ) = a : = by
have : = t mod_add_t div a b ; rwa [ H , Int . zero_add ] at this
theorem div_mul_cancel_of_mod_eq_zero { a b : Int } ( H : a . mod b = 0 ) : a . div b * b = a : = by
rw [ Int . mul_comm , mul_div_cancel_of_mod_eq_zero H ]
theorem t div_mul_cancel_of_t mod_eq_zero { a b : Int } ( H : a . t mod b = 0 ) : a . t div b * b = a : = by
rw [ Int . mul_comm , mul_t div_cancel_of_t mod_eq_zero H ]
theorem dvd_of_mod_eq_zero { a b : Int } ( H : mod b a = 0 ) : a ∣ b : =
⟨ b . div a , ( mul_div_cancel_of_mod_eq_zero H ) . symm ⟩
theorem dvd_of_t mod_eq_zero { a b : Int } ( H : t mod b a = 0 ) : a ∣ b : =
⟨ b . t div a , ( mul_t div_cancel_of_t mod_eq_zero H ) . symm ⟩
protected theorem mul_div_assoc ( a : Int ) : ∀ { b c : Int } , c ∣ b → ( a * b ) . div c = a * ( b . div c )
protected theorem mul_t div_assoc ( a : Int ) : ∀ { b c : Int } , c ∣ b → ( a * b ) . t div c = a * ( b . t div c )
| _ , c , ⟨ d , rfl ⟩ = >
if cz : c = 0 then by simp [ cz , Int . mul_zero ] else by
rw [ Int . mul_left_comm , Int . mul_div_cancel_left _ cz , Int . mul_div_cancel_left _ cz ]
rw [ Int . mul_left_comm , Int . mul_t div_cancel_left _ cz , Int . mul_t div_cancel_left _ cz ]
protected theorem mul_div_assoc' ( b : Int ) { a c : Int } ( h : c ∣ a ) :
( a * b ) . div c = a . div c * b : = by
rw [ Int . mul_comm , Int . mul_div_assoc _ h , Int . mul_comm ]
protected theorem mul_t div_assoc' ( b : Int ) { a c : Int } ( h : c ∣ a ) :
( a * b ) . t div c = a . t div c * b : = by
rw [ Int . mul_comm , Int . mul_t div_assoc _ h , Int . mul_comm ]
theorem div_dvd_div : ∀ { a b c : Int } , a ∣ b → b ∣ c → b . div a ∣ c . div a
theorem t div_dvd_t div : ∀ { a b c : Int } , a ∣ b → b ∣ c → b . t div a ∣ c . t div a
| a , _ , _ , ⟨ b , rfl ⟩ , ⟨ c , rfl ⟩ = > by
by_cases az : a = 0
· simp [ az ]
· rw [ Int . mul_div_cancel_left _ az , Int . mul_assoc , Int . mul_div_cancel_left _ az ]
· rw [ Int . mul_t div_cancel_left _ az , Int . mul_assoc , Int . mul_t div_cancel_left _ az ]
apply Int . dvd_mul_right
@[ simp ] theorem natAbs_div ( a b : Int ) : natAbs ( a . div b ) = ( natAbs a ) . div ( natAbs b ) : =
@[ simp ] theorem natAbs_t div ( a b : Int ) : natAbs ( a . t div b ) = ( natAbs a ) . div ( natAbs b ) : =
match a , b , eq_nat_or_neg a , eq_nat_or_neg b with
| _ , _ , ⟨ _ , . inl rfl ⟩ , ⟨ _ , . inl rfl ⟩ = > rfl
| _ , _ , ⟨ _ , . inl rfl ⟩ , ⟨ _ , . inr rfl ⟩ = > by rw [ Int . div_neg , natAbs_neg , natAbs_neg ] ; rfl
| _ , _ , ⟨ _ , . inr rfl ⟩ , ⟨ _ , . inl rfl ⟩ = > by rw [ Int . neg_div , natAbs_neg , natAbs_neg ] ; rfl
| _ , _ , ⟨ _ , . inr rfl ⟩ , ⟨ _ , . inr rfl ⟩ = > by rw [ Int . neg_div_neg , natAbs_neg , natAbs_neg ] ; rfl
| _ , _ , ⟨ _ , . inl rfl ⟩ , ⟨ _ , . inr rfl ⟩ = > by rw [ Int . t div_neg, natAbs_neg , natAbs_neg ] ; rfl
| _ , _ , ⟨ _ , . inr rfl ⟩ , ⟨ _ , . inl rfl ⟩ = > by rw [ Int . neg_t div , natAbs_neg , natAbs_neg ] ; rfl
| _ , _ , ⟨ _ , . inr rfl ⟩ , ⟨ _ , . inr rfl ⟩ = > by rw [ Int . neg_t div_neg , natAbs_neg , natAbs_neg ] ; rfl
protected theorem div_eq_of_eq_mul_right { a b c : Int }
( H1 : b ≠ 0 ) ( H2 : a = b * c ) : a . div b = c : = by rw [ H2 , Int . mul_div_cancel_left _ H1 ]
protected theorem t div_eq_of_eq_mul_right { a b c : Int }
( H1 : b ≠ 0 ) ( H2 : a = b * c ) : a . t div b = c : = by rw [ H2 , Int . mul_t div_cancel_left _ H1 ]
protected theorem eq_div_of_mul_eq_right { a b c : Int }
( H1 : a ≠ 0 ) ( H2 : a * b = c ) : b = c . div a : =
( Int . div_eq_of_eq_mul_right H1 H2 . symm ) . symm
protected theorem eq_t div_of_mul_eq_right { a b c : Int }
( H1 : a ≠ 0 ) ( H2 : a * b = c ) : b = c . t div a : =
( Int . t div_eq_of_eq_mul_right H1 H2 . symm ) . symm
/- ! ### (t - )mod -/
theorem ofNat_mod ( m n : Nat ) : ( ↑ ( m % n ) : Int ) = mod m n : = rfl
theorem ofNat_t mod ( m n : Nat ) : ( ↑ ( m % n ) : Int ) = t mod m n : = rfl
@[ simp ] theorem mod_one ( a : Int ) : mod a 1 = 0 : = by
simp [ mod_def , Int . div_one , Int . one_mul , Int . sub_self ]
@[ simp ] theorem t mod_one ( a : Int ) : t mod a 1 = 0 : = by
simp [ t mod_def, Int . t div_one, Int . one_mul , Int . sub_self ]
theorem mod_eq_of_lt { a b : Int } ( H1 : 0 ≤ a ) ( H2 : a < b ) : mod a b = a : = by
rw [ mod_eq_emod H1 ( Int . le_trans H1 ( Int . le_of_lt H2 ) ) , emod_eq_of_lt H1 H2 ]
theorem t mod_eq_of_lt { a b : Int } ( H1 : 0 ≤ a ) ( H2 : a < b ) : t mod a b = a : = by
rw [ t mod_eq_emod H1 ( Int . le_trans H1 ( Int . le_of_lt H2 ) ) , emod_eq_of_lt H1 H2 ]
theorem mod_lt_of_pos ( a : Int ) { b : Int } ( H : 0 < b ) : mod a b < b : =
theorem t mod_lt_of_pos ( a : Int ) { b : Int } ( H : 0 < b ) : t mod a b < b : =
match a , b , eq_succ_of_zero_lt H with
| ofNat _ , _ , ⟨ n , rfl ⟩ = > ofNat_lt . 2 < | Nat . mod_lt _ n . succ_pos
| - [ _ + 1 ] , _ , ⟨ n , rfl ⟩ = > Int . lt_of_le_of_lt
( Int . neg_nonpos_of_nonneg < | Int . ofNat_nonneg _ ) ( ofNat_pos . 2 n . succ_pos )
theorem mod_nonneg : ∀ { a : Int } ( b : Int ) , 0 ≤ a → 0 ≤ mod a b
theorem t mod_nonneg : ∀ { a : Int } ( b : Int ) , 0 ≤ a → 0 ≤ t mod a b
| ofNat _ , - [ _ + 1 ] , _ | ofNat _ , ofNat _ , _ = > ofNat_nonneg _
@[ simp ] theorem mod_neg ( a b : Int ) : mod a ( - b ) = mod a b : = by
rw [ mod_def , mod_def , Int . div_neg , Int . neg_mul_neg ]
@[ simp ] theorem t mod_neg ( a b : Int ) : t mod a ( - b ) = t mod a b : = by
rw [ t mod_def, t mod_def, Int . t div_neg, Int . neg_mul_neg ]
@[ simp ] theorem mul_mod_left ( a b : Int ) : ( a * b ) . mod b = 0 : =
@[ simp ] theorem mul_t mod_left ( a b : Int ) : ( a * b ) . t mod b = 0 : =
if h : b = 0 then by simp [ h , Int . mul_zero ] else by
rw [ Int . mod_def , Int . mul_div_cancel _ h , Int . mul_comm , Int . sub_self ]
rw [ Int . t mod_def, Int . mul_t div_cancel _ h , Int . mul_comm , Int . sub_self ]
@[ simp ] theorem mul_mod_right ( a b : Int ) : ( a * b ) . mod a = 0 : = by
rw [ Int . mul_comm , mul_mod_left ]
@[ simp ] theorem mul_t mod_right ( a b : Int ) : ( a * b ) . t mod a = 0 : = by
rw [ Int . mul_comm , mul_t mod_left ]
theorem mod_eq_zero_of_dvd : ∀ { a b : Int } , a ∣ b → mod b a = 0
| _ , _ , ⟨ _ , rfl ⟩ = > mul_mod_right . .
theorem t mod_eq_zero_of_dvd : ∀ { a b : Int } , a ∣ b → t mod b a = 0
| _ , _ , ⟨ _ , rfl ⟩ = > mul_t mod_right . .
theorem dvd_iff_mod_eq_zero { a b : Int } : a ∣ b ↔ mod b a = 0 : =
⟨ mod_eq_zero_of_dvd , dvd_of_mod_eq_zero ⟩
theorem dvd_iff_t mod_eq_zero { a b : Int } : a ∣ b ↔ t mod b a = 0 : =
⟨ t mod_eq_zero_of_dvd, dvd_of_t mod_eq_zero ⟩
@[ simp ] theorem neg_mul_mod_right ( a b : Int ) : ( - ( a * b ) ) . mod a = 0 : = by
rw [ ← dvd_iff_mod_eq_zero , Int . dvd_neg ]
@[ simp ] theorem neg_mul_t mod_right ( a b : Int ) : ( - ( a * b ) ) . t mod a = 0 : = by
rw [ ← dvd_iff_t mod_eq_zero , Int . dvd_neg ]
exact Int . dvd_mul_right a b
@[ simp ] theorem neg_mul_mod_left ( a b : Int ) : ( - ( a * b ) ) . mod b = 0 : = by
rw [ ← dvd_iff_mod_eq_zero , Int . dvd_neg ]
@[ simp ] theorem neg_mul_t mod_left ( a b : Int ) : ( - ( a * b ) ) . t mod b = 0 : = by
rw [ ← dvd_iff_t mod_eq_zero , Int . dvd_neg ]
exact Int . dvd_mul_left a b
protected theorem div_mul_cancel { a b : Int } ( H : b ∣ a ) : a . div b * b = a : =
div_mul_cancel_of_mod_eq_zero ( mod_eq_zero_of_dvd H )
protected theorem t div_mul_cancel { a b : Int } ( H : b ∣ a ) : a . t div b * b = a : =
t div_mul_cancel_of_t mod_eq_zero ( t mod_eq_zero_of_dvd H )
protected theorem mul_div_cancel' { a b : Int } ( H : a ∣ b ) : a * b . div a = b : = by
rw [ Int . mul_comm , Int . div_mul_cancel H ]
protected theorem mul_t div_cancel' { a b : Int } ( H : a ∣ b ) : a * b . t div a = b : = by
rw [ Int . mul_comm , Int . t div_mul_cancel H ]
protected theorem eq_mul_of_div_eq_right { a b c : Int }
( H1 : b ∣ a ) ( H2 : a . div b = c ) : a = b * c : = by rw [ ← H2 , Int . mul_div_cancel' H1 ]
protected theorem eq_mul_of_t div_eq_right { a b c : Int }
( H1 : b ∣ a ) ( H2 : a . t div b = c ) : a = b * c : = by rw [ ← H2 , Int . mul_t div_cancel' H1 ]
@[ simp ] theorem mod_self { a : Int } : a . mod a = 0 : = by
have : = mul_mod_left 1 a ; rwa [ Int . one_mul ] at this
@[ simp ] theorem t mod_self { a : Int } : a . t mod a = 0 : = by
have : = mul_t mod_left 1 a ; rwa [ Int . one_mul ] at this
@[ simp ] theorem neg_mod_self ( a : Int ) : ( - a ) . mod a = 0 : = by
rw [ ← dvd_iff_mod_eq_zero , Int . dvd_neg ]
@[ simp ] theorem neg_t mod_self ( a : Int ) : ( - a ) . t mod a = 0 : = by
rw [ ← dvd_iff_t mod_eq_zero , Int . dvd_neg ]
exact Int . dvd_refl a
theorem lt_div_add_one_mul_self ( a : Int ) { b : Int } ( H : 0 < b ) : a < ( a . div b + 1 ) * b : = by
theorem lt_t div_add_one_mul_self ( a : Int ) { b : Int } ( H : 0 < b ) : a < ( a . t div b + 1 ) * b : = by
rw [ Int . add_mul , Int . one_mul , Int . mul_comm ]
exact Int . lt_add_of_sub_left_lt < | Int . mod_def . . ▸ mod_lt_of_pos _ H
exact Int . lt_add_of_sub_left_lt < | Int . t mod_def . . ▸ t mod_lt_of_pos _ H
protected theorem div_eq_iff_eq_mul_right { a b c : Int }
( H : b ≠ 0 ) ( H' : b ∣ a ) : a . div b = c ↔ a = b * c : =
⟨ Int . eq_mul_of_div_eq_right H' , Int . div_eq_of_eq_mul_right H ⟩
protected theorem t div_eq_iff_eq_mul_right { a b c : Int }
( H : b ≠ 0 ) ( H' : b ∣ a ) : a . t div b = c ↔ a = b * c : =
⟨ Int . eq_mul_of_t div_eq_right H' , Int . t div_eq_of_eq_mul_right H ⟩
protected theorem div_eq_iff_eq_mul_left { a b c : Int }
( H : b ≠ 0 ) ( H' : b ∣ a ) : a . div b = c ↔ a = c * b : = by
rw [ Int . mul_comm ] ; exact Int . div_eq_iff_eq_mul_right H H'
protected theorem t div_eq_iff_eq_mul_left { a b c : Int }
( H : b ≠ 0 ) ( H' : b ∣ a ) : a . t div b = c ↔ a = c * b : = by
rw [ Int . mul_comm ] ; exact Int . t div_eq_iff_eq_mul_right H H'
protected theorem eq_mul_of_div_eq_left { a b c : Int }
( H1 : b ∣ a ) ( H2 : a . div b = c ) : a = c * b : = by
rw [ Int . mul_comm , Int . eq_mul_of_div_eq_right H1 H2 ]
protected theorem eq_mul_of_t div_eq_left { a b c : Int }
( H1 : b ∣ a ) ( H2 : a . t div b = c ) : a = c * b : = by
rw [ Int . mul_comm , Int . eq_mul_of_t div_eq_right H1 H2 ]
protected theorem div_eq_of_eq_mul_left { a b c : Int }
( H1 : b ≠ 0 ) ( H2 : a = c * b ) : a . div b = c : =
Int . div_eq_of_eq_mul_right H1 ( by rw [ Int . mul_comm , H2 ] )
protected theorem t div_eq_of_eq_mul_left { a b c : Int }
( H1 : b ≠ 0 ) ( H2 : a = c * b ) : a . t div b = c : =
Int . t div_eq_of_eq_mul_right H1 ( by rw [ Int . mul_comm , H2 ] )
protected theorem eq_zero_of_div_eq_zero { d n : Int } ( h : d ∣ n ) ( H : n . div d = 0 ) : n = 0 : = by
rw [ ← Int . mul_div_cancel' h , H , Int . mul_zero ]
protected theorem eq_zero_of_t div_eq_zero { d n : Int } ( h : d ∣ n ) ( H : n . t div d = 0 ) : n = 0 : = by
rw [ ← Int . mul_t div_cancel' h , H , Int . mul_zero ]
@[ simp ] protected theorem div_left_inj { a b d : Int }
( hda : d ∣ a ) ( hdb : d ∣ b ) : a . div d = b . div d ↔ a = b : = by
refine ⟨ fun h = > ? _ , congrArg ( div · d ) ⟩
rw [ ← Int . mul_div_cancel' hda , ← Int . mul_div_cancel' hdb , h ]
@[ simp ] protected theorem t div_left_inj { a b d : Int }
( hda : d ∣ a ) ( hdb : d ∣ b ) : a . t div d = b . t div d ↔ a = b : = by
refine ⟨ fun h = > ? _ , congrArg ( t div · d ) ⟩
rw [ ← Int . mul_t div_cancel' hda , ← Int . mul_t div_cancel' hdb , h ]
theorem div_sign : ∀ a b , a . div ( sign b ) = a * sign b
theorem t div_sign : ∀ a b , a . t div ( sign b ) = a * sign b
| _ , succ _ = > by simp [ sign , Int . mul_one ]
| _ , 0 = > by simp [ sign , Int . mul_zero ]
| _ , - [ _ + 1 ] = > by simp [ sign , Int . mul_neg , Int . mul_one ]
protected theorem sign_eq_div_abs ( a : Int ) : sign a = a . div ( natAbs a ) : =
protected theorem sign_eq_t div_abs ( a : Int ) : sign a = a . t div ( natAbs a ) : =
if az : a = 0 then by simp [ az ] else
( Int . div_eq_of_eq_mul_left ( ofNat_ne_zero . 2 < | natAbs_ne_zero . 2 az )
( Int . t div_eq_of_eq_mul_left ( ofNat_ne_zero . 2 < | natAbs_ne_zero . 2 az )
( sign_mul_natAbs _ ) . symm ) . symm
/- ! ### fdiv -/
@@ -1033,7 +1034,7 @@ theorem fmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.fmod b = a :=
rw [ fmod_eq_emod _ ( Int . le_trans H1 ( Int . le_of_lt H2 ) ) , emod_eq_of_lt H1 H2 ]
theorem fmod_nonneg { a b : Int } ( ha : 0 ≤ a ) ( hb : 0 ≤ b ) : 0 ≤ a . fmod b : =
fmod_eq_mod ha hb ▸ mod_nonneg _ ha
fmod_eq_t mod ha hb ▸ t mod_nonneg _ ha
theorem fmod_nonneg' ( a : Int ) { b : Int } ( hb : 0 < b ) : 0 ≤ a . fmod b : =
fmod_eq_emod _ ( Int . le_of_lt hb ) ▸ emod_nonneg _ ( Int . ne_of_lt hb ) . symm
@@ -1053,10 +1054,10 @@ theorem fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.fmod b < b :=
/- ! ### Theorems crossing div / mod versions -/
theorem div_eq_ediv_of_dvd { a b : Int } ( h : b ∣ a ) : a . div b = a / b : = by
theorem t div_eq_ediv_of_dvd { a b : Int } ( h : b ∣ a ) : a . t div b = a / b : = by
by_cases b0 : b = 0
· simp [ b0 ]
· rw [ Int . div_eq_iff_eq_mul_left b0 h , ← Int . ediv_eq_iff_eq_mul_left b0 h ]
· rw [ Int . t div_eq_iff_eq_mul_left b0 h , ← Int . ediv_eq_iff_eq_mul_left b0 h ]
theorem fdiv_eq_ediv_of_dvd : ∀ { a b : Int } , b ∣ a → a . fdiv b = a / b
| _ , b , ⟨ c , rfl ⟩ = > by
@@ -1268,3 +1269,65 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
all_goals decide
· exact ofNat_nonneg x
· exact succ_ofNat_pos ( x + 1 )
/- ! ### Deprecations -/
@[ deprecated Int . zero_tdiv ( since : = " 2024-09-11 " ) ] protected abbrev zero_div : = @ Int . zero_tdiv
@[ deprecated Int . tdiv_zero ( since : = " 2024-09-11 " ) ] protected abbrev div_zero : = @ Int . tdiv_zero
@[ deprecated tdiv_eq_ediv ( since : = " 2024-09-11 " ) ] abbrev div_eq_ediv : = @ tdiv_eq_ediv
@[ deprecated fdiv_eq_tdiv ( since : = " 2024-09-11 " ) ] abbrev fdiv_eq_div : = @ fdiv_eq_tdiv
@[ deprecated zero_tmod ( since : = " 2024-09-11 " ) ] abbrev zero_mod : = @ zero_tmod
@[ deprecated tmod_zero ( since : = " 2024-09-11 " ) ] abbrev mod_zero : = @ tmod_zero
@[ deprecated tmod_add_tdiv ( since : = " 2024-09-11 " ) ] abbrev mod_add_div : = @ tmod_add_tdiv
@[ deprecated tdiv_add_tmod ( since : = " 2024-09-11 " ) ] abbrev div_add_mod : = @ tdiv_add_tmod
@[ deprecated tmod_add_tdiv' ( since : = " 2024-09-11 " ) ] abbrev mod_add_div' : = @ tmod_add_tdiv'
@[ deprecated tdiv_add_tmod' ( since : = " 2024-09-11 " ) ] abbrev div_add_mod' : = @ tdiv_add_tmod'
@[ deprecated tmod_def ( since : = " 2024-09-11 " ) ] abbrev mod_def : = @ tmod_def
@[ deprecated tmod_eq_emod ( since : = " 2024-09-11 " ) ] abbrev mod_eq_emod : = @ tmod_eq_emod
@[ deprecated fmod_eq_tmod ( since : = " 2024-09-11 " ) ] abbrev fmod_eq_mod : = @ fmod_eq_tmod
@[ deprecated Int . tdiv_one ( since : = " 2024-09-11 " ) ] protected abbrev div_one : = @ Int . tdiv_one
@[ deprecated Int . tdiv_neg ( since : = " 2024-09-11 " ) ] protected abbrev div_neg : = @ Int . tdiv_neg
@[ deprecated Int . neg_tdiv ( since : = " 2024-09-11 " ) ] protected abbrev neg_div : = @ Int . neg_tdiv
@[ deprecated Int . neg_tdiv_neg ( since : = " 2024-09-11 " ) ] protected abbrev neg_div_neg : = @ Int . neg_tdiv_neg
@[ deprecated Int . tdiv_nonneg ( since : = " 2024-09-11 " ) ] protected abbrev div_nonneg : = @ Int . tdiv_nonneg
@[ deprecated Int . tdiv_nonpos ( since : = " 2024-09-11 " ) ] protected abbrev div_nonpos : = @ Int . tdiv_nonpos
@[ deprecated Int . tdiv_eq_zero_of_lt ( since : = " 2024-09-11 " ) ] abbrev div_eq_zero_of_lt : = @ Int . tdiv_eq_zero_of_lt
@[ deprecated Int . mul_tdiv_cancel ( since : = " 2024-09-11 " ) ] protected abbrev mul_div_cancel : = @ Int . mul_tdiv_cancel
@[ deprecated Int . mul_tdiv_cancel_left ( since : = " 2024-09-11 " ) ] protected abbrev mul_div_cancel_left : = @ Int . mul_tdiv_cancel_left
@[ deprecated Int . tdiv_self ( since : = " 2024-09-11 " ) ] protected abbrev div_self : = @ Int . tdiv_self
@[ deprecated Int . mul_tdiv_cancel_of_tmod_eq_zero ( since : = " 2024-09-11 " ) ] abbrev mul_div_cancel_of_mod_eq_zero : = @ Int . mul_tdiv_cancel_of_tmod_eq_zero
@[ deprecated Int . tdiv_mul_cancel_of_tmod_eq_zero ( since : = " 2024-09-11 " ) ] abbrev div_mul_cancel_of_mod_eq_zero : = @ Int . tdiv_mul_cancel_of_tmod_eq_zero
@[ deprecated Int . dvd_of_tmod_eq_zero ( since : = " 2024-09-11 " ) ] abbrev dvd_of_mod_eq_zero : = @ Int . dvd_of_tmod_eq_zero
@[ deprecated Int . mul_tdiv_assoc ( since : = " 2024-09-11 " ) ] protected abbrev mul_div_assoc : = @ Int . mul_tdiv_assoc
@[ deprecated Int . mul_tdiv_assoc' ( since : = " 2024-09-11 " ) ] protected abbrev mul_div_assoc' : = @ Int . mul_tdiv_assoc'
@[ deprecated Int . tdiv_dvd_tdiv ( since : = " 2024-09-11 " ) ] abbrev div_dvd_div : = @ Int . tdiv_dvd_tdiv
@[ deprecated Int . natAbs_tdiv ( since : = " 2024-09-11 " ) ] abbrev natAbs_div : = @ Int . natAbs_tdiv
@[ deprecated Int . tdiv_eq_of_eq_mul_right ( since : = " 2024-09-11 " ) ] protected abbrev div_eq_of_eq_mul_right : = @ Int . tdiv_eq_of_eq_mul_right
@[ deprecated Int . eq_tdiv_of_mul_eq_right ( since : = " 2024-09-11 " ) ] protected abbrev eq_div_of_mul_eq_right : = @ Int . eq_tdiv_of_mul_eq_right
@[ deprecated Int . ofNat_tmod ( since : = " 2024-09-11 " ) ] abbrev ofNat_mod : = @ Int . ofNat_tmod
@[ deprecated Int . tmod_one ( since : = " 2024-09-11 " ) ] abbrev mod_one : = @ Int . tmod_one
@[ deprecated Int . tmod_eq_of_lt ( since : = " 2024-09-11 " ) ] abbrev mod_eq_of_lt : = @ Int . tmod_eq_of_lt
@[ deprecated Int . tmod_lt_of_pos ( since : = " 2024-09-11 " ) ] abbrev mod_lt_of_pos : = @ Int . tmod_lt_of_pos
@[ deprecated Int . tmod_nonneg ( since : = " 2024-09-11 " ) ] abbrev mod_nonneg : = @ Int . tmod_nonneg
@[ deprecated Int . tmod_neg ( since : = " 2024-09-11 " ) ] abbrev mod_neg : = @ Int . tmod_neg
@[ deprecated Int . mul_tmod_left ( since : = " 2024-09-11 " ) ] abbrev mul_mod_left : = @ Int . mul_tmod_left
@[ deprecated Int . mul_tmod_right ( since : = " 2024-09-11 " ) ] abbrev mul_mod_right : = @ Int . mul_tmod_right
@[ deprecated Int . tmod_eq_zero_of_dvd ( since : = " 2024-09-11 " ) ] abbrev mod_eq_zero_of_dvd : = @ Int . tmod_eq_zero_of_dvd
@[ deprecated Int . dvd_iff_tmod_eq_zero ( since : = " 2024-09-11 " ) ] abbrev dvd_iff_mod_eq_zero : = @ Int . dvd_iff_tmod_eq_zero
@[ deprecated Int . neg_mul_tmod_right ( since : = " 2024-09-11 " ) ] abbrev neg_mul_mod_right : = @ Int . neg_mul_tmod_right
@[ deprecated Int . neg_mul_tmod_left ( since : = " 2024-09-11 " ) ] abbrev neg_mul_mod_left : = @ Int . neg_mul_tmod_left
@[ deprecated Int . tdiv_mul_cancel ( since : = " 2024-09-11 " ) ] protected abbrev div_mul_cancel : = @ Int . tdiv_mul_cancel
@[ deprecated Int . mul_tdiv_cancel' ( since : = " 2024-09-11 " ) ] protected abbrev mul_div_cancel' : = @ Int . mul_tdiv_cancel'
@[ deprecated Int . eq_mul_of_tdiv_eq_right ( since : = " 2024-09-11 " ) ] protected abbrev eq_mul_of_div_eq_right : = @ Int . eq_mul_of_tdiv_eq_right
@[ deprecated Int . tmod_self ( since : = " 2024-09-11 " ) ] abbrev mod_self : = @ Int . tmod_self
@[ deprecated Int . neg_tmod_self ( since : = " 2024-09-11 " ) ] abbrev neg_mod_self : = @ Int . neg_tmod_self
@[ deprecated Int . lt_tdiv_add_one_mul_self ( since : = " 2024-09-11 " ) ] abbrev lt_div_add_one_mul_self : = @ Int . lt_tdiv_add_one_mul_self
@[ deprecated Int . tdiv_eq_iff_eq_mul_right ( since : = " 2024-09-11 " ) ] protected abbrev div_eq_iff_eq_mul_right : = @ Int . tdiv_eq_iff_eq_mul_right
@[ deprecated Int . tdiv_eq_iff_eq_mul_left ( since : = " 2024-09-11 " ) ] protected abbrev div_eq_iff_eq_mul_left : = @ Int . tdiv_eq_iff_eq_mul_left
@[ deprecated Int . eq_mul_of_tdiv_eq_left ( since : = " 2024-09-11 " ) ] protected abbrev eq_mul_of_div_eq_left : = @ Int . eq_mul_of_tdiv_eq_left
@[ deprecated Int . tdiv_eq_of_eq_mul_left ( since : = " 2024-09-11 " ) ] protected abbrev div_eq_of_eq_mul_left : = @ Int . tdiv_eq_of_eq_mul_left
@[ deprecated Int . eq_zero_of_tdiv_eq_zero ( since : = " 2024-09-11 " ) ] protected abbrev eq_zero_of_div_eq_zero : = @ Int . eq_zero_of_tdiv_eq_zero
@[ deprecated Int . tdiv_left_inj ( since : = " 2024-09-11 " ) ] protected abbrev div_left_inj : = @ Int . tdiv_left_inj
@[ deprecated Int . tdiv_sign ( since : = " 2024-09-11 " ) ] abbrev div_sign : = @ Int . tdiv_sign
@[ deprecated Int . sign_eq_tdiv_abs ( since : = " 2024-09-11 " ) ] protected abbrev sign_eq_div_abs : = @ Int . sign_eq_tdiv_abs
@[ deprecated Int . tdiv_eq_ediv_of_dvd ( since : = " 2024-09-11 " ) ] abbrev div_eq_ediv_of_dvd : = @ Int . tdiv_eq_ediv_of_dvd
