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
! This file was ported from Lean 3 source module data.int.char_zero
! leanprover-community/mathlib commit 29cb56a7b35f72758b05a30490e1f10bd62c35c1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Int.Cast.Field
/-!
# Injectivity of `Int.Cast` into characteristic zero rings and fields.
-/
variable { α : Type _ }
open Nat
namespace Int
@[ simp ]
theorem cast_eq_zero [ AddGroupWithOne α ] [ CharZero α ] { n : ℤ } : ( n : α ) = 0 ↔ n = 0 :=
⟨ fun h => by
cases n
· erw [ Int.cast_ofNat ] at h
exact congr_arg : ∀ {α : Sort ?u.748} {β : Sort ?u.747} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ _ ( Nat.cast_eq_zero . 1 : ∀ {a b : Prop }, (a ↔ b a → b h )
· rw [ cast_negSucc , neg_eq_zero , Nat.cast_eq_zero ] at h
contradiction ,
fun h => by rw [ h , cast_zero ] ⟩
#align int.cast_eq_zero Int.cast_eq_zero
@[ simp , norm_cast ]
theorem cast_inj [ AddGroupWithOne : Type ?u.1176 → Type ?u.1176 α ] [ CharZero α ] { m n : ℤ } : ( m : α ) = n ↔ m = n := by
rw [ ← sub_eq_zero : ∀ {G : Type ?u.1520} [inst : AddGroup G a b : G }, a - b = 0 ↔ a = b , ← cast_sub , cast_eq_zero , sub_eq_zero : ∀ {G : Type ?u.1639} [inst : AddGroup G a b : G }, a - b = 0 ↔ a = b ]
#align int.cast_inj Int.cast_inj
theorem cast_injective [ AddGroupWithOne : Type ?u.1809 → Type ?u.1809 α ] [ CharZero α ] : Function.Injective : {α : Sort ?u.1829} → {β : Sort ?u.1828} → (α → β Prop ( Int.cast : ℤ → α )
| _, _ => cast_inj . 1 : ∀ {a b : Prop }, (a ↔ b a → b
#align int.cast_injective Int.cast_injective
theorem cast_ne_zero [ AddGroupWithOne : Type ?u.2072 → Type ?u.2072 α ] [ CharZero α ] { n : ℤ } : ( n : α ) ≠ 0 ↔ n ≠ 0 :=
not_congr : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b cast_eq_zero
#align int.cast_ne_zero Int.cast_ne_zero
@[ simp ]
theorem cast_eq_one [ AddGroupWithOne : Type ?u.2680 → Type ?u.2680 α ] [ CharZero α ] { n : ℤ } : ( n : α ) = 1 ↔ n = 1 := by
rw [ ← cast_one , cast_inj ]
#align int.cast_eq_one Int.cast_eq_one
theorem cast_ne_one [ AddGroupWithOne : Type ?u.3193 → Type ?u.3193 α ] [ CharZero α ] { n : ℤ } : ( n : α ) ≠ 1 ↔ n ≠ 1 :=
cast_eq_one . not : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b
#align int.cast_ne_one Int.cast_ne_one
@[ simp , norm_cast ]
theorem cast_div_charZero { k : Type _ } [ DivisionRing : Type ?u.3621 → Type ?u.3621 k ] [ CharZero k ] { m n : ℤ } ( n_dvd : n ∣ m ) :
(( m / n : ℤ ) : k ) = m / n := by
rcases eq_or_ne : ∀ {α : Sort ?u.4000} (x y : α ), x = y ∨ x ≠ y n 0 with (rfl | hn) : n = 0 ∨ n ≠ 0 rfl | hn (rfl | hn) : n = 0 ∨ n ≠ 0
· simp [ Int.ediv_zero : ∀ (a : ℤ ), a / 0 = 0 ]
· exact cast_div n_dvd ( cast_ne_zero . mpr : ∀ {a b : Prop }, (a ↔ b b → a hn )
#align int.cast_div_char_zero Int.cast_div_charZero
end Int
theorem RingHom.injective_int { α : Type _ } [ NonAssocRing : Type ?u.4667 → Type ?u.4667 α ] ( f : ℤ →+* α ) [ CharZero α ] :
Function.Injective : {α : Sort ?u.4941} → {β : Sort ?u.4940} → (α → β Prop f :=
Subsingleton.elim ( Int.castRingHom _ ) f ▸ Int.cast_injective
#align ring_hom.injective_int RingHom.injective_int