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) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad
! This file was ported from Lean 3 source module data.int.div
! leanprover-community/mathlib commit ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Int.Dvd.Basic
import Mathlib.Data.Nat.Order.Lemmas
import Mathlib.Algebra.Ring.Regular
/-!
# Lemmas relating `/` in `β€` with the ordering.
-/
open Nat
namespace Int
theorem eq_mul_div_of_mul_eq_mul_of_dvd_left : β {a b c d : β€ }, b β 0 b β£ c b * a = c * d a = c / b * d eq_mul_div_of_mul_eq_mul_of_dvd_left { a b c d : β€ } ( hb : b β 0 ) ( hbc : b β£ c )
( h : b * a = c * d ) : a = c / b * d := by
cases' hbc with k hk
subst hk
rw [ Int.mul_ediv_cancel_left : β {a : β€ } (b : β€ ), a β 0 a * b / a = b _ hb ]
rw [ mul_assoc : β {G : Type ?u.307} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c ] at h
apply mul_left_cancelβ hb h
#align int.eq_mul_div_of_mul_eq_mul_of_dvd_left Int.eq_mul_div_of_mul_eq_mul_of_dvd_left : β {a b c d : β€ }, b β 0 b β£ c b * a = c * d a = c / b * d
/-- If an integer with larger absolute value divides an integer, it is
zero. -/
theorem eq_zero_of_dvd_of_natAbs_lt_natAbs { a b : β€ } ( w : a β£ b ) ( h : natAbs b < natAbs a ) :
b = 0 := by
rw [ β natAbs_dvd , β dvd_natAbs , coe_nat_dvd ] at w
rw [ β natAbs_eq_zero ]
exact eq_zero_of_dvd_of_lt : β {a b : β }, a β£ b b < a b = 0 w h
#align int.eq_zero_of_dvd_of_nat_abs_lt_nat_abs Int.eq_zero_of_dvd_of_natAbs_lt_natAbs
theorem eq_zero_of_dvd_of_nonneg_of_lt : β {a b : β€ }, 0 β€ a a < b b β£ a a = 0 eq_zero_of_dvd_of_nonneg_of_lt { a b : β€ } ( wβ : 0 β€ a ) ( wβ : a < b ) ( h : b β£ a ) : a = 0 :=
eq_zero_of_dvd_of_natAbs_lt_natAbs h ( natAbs_lt_natAbs_of_nonneg_of_lt wβ wβ )
#align int.eq_zero_of_dvd_of_nonneg_of_lt Int.eq_zero_of_dvd_of_nonneg_of_lt : β {a b : β€ }, 0 β€ a a < b b β£ a a = 0
/-- If two integers are congruent to a sufficiently large modulus,
they are equal. -/
theorem eq_of_mod_eq_of_natAbs_sub_lt_natAbs : β {a b c : β€ }, a % b = c natAbs (a - c < natAbs b a = c eq_of_mod_eq_of_natAbs_sub_lt_natAbs { a b c : β€ } ( h1 : a % b = c )
( h2 : natAbs ( a - c ) < natAbs b ) : a = c :=
eq_of_sub_eq_zero ( eq_zero_of_dvd_of_natAbs_lt_natAbs ( dvd_sub_of_emod_eq : β {a b c : β€ }, a % b = c b β£ a - c h1 ) h2 )
#align int.eq_of_mod_eq_of_nat_abs_sub_lt_nat_abs Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs : β {a b c : β€ }, a % b = c natAbs (a - c < natAbs b a = c
theorem ofNat_add_negSucc_of_ge { m n : β } ( h : n . succ β€ m ) :
ofNat m + -[ n +1] = ofNat ( m - n . succ ) := by
rw [ negSucc_eq , ofNat_eq_cast , ofNat_eq_cast , β Nat.cast_one , β Nat.cast_add ,
β sub_eq_add_neg , β Nat.cast_sub h ]
#align int.of_nat_add_neg_succ_of_nat_of_ge Int.ofNat_add_negSucc_of_ge
theorem natAbs_le_of_dvd_ne_zero { s t : β€ } ( hst : s β£ t ) ( ht : t β 0 ) : natAbs s β€ natAbs t :=
not_lt . mp : β {a b : Prop }, (a β b a β b ( mt : β {a b : Prop }, (a β b Β¬ b Β¬ a ( eq_zero_of_dvd_of_natAbs_lt_natAbs hst ) ht )
#align int.nat_abs_le_of_dvd_ne_zero Int.natAbs_le_of_dvd_ne_zero
end Int