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 Cmdinstead 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
Ported by: Scott Morrison

! This file was ported from Lean 3 source module data.int.cast.lemmas
! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Int.Order.Basic
import Mathlib.Data.Nat.Cast.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`),
particularly results involving algebraic homomorphisms or the order structure on `ℤ`
which were not available in the import dependencies of `Data.Int.Cast.Basic`.

## Main declarations

* `castAddHom`: `cast` bundled as an `AddMonoidHom`.
* `castRingHom`: `cast` bundled as a `RingHom`.
-/


open Nat

variable {
F: Type ?u.34761
F
ι: Type ?u.15852
ι
α: Type ?u.15855
α
β: Type ?u.23
β
:
Type _: Type (?u.68416+1)
Type _
} namespace Int /-- Coercion `ℕ → ℤ` as a `RingHom`. -/ def ofNatHom :
ℕ: Type
ℕ
→+*
ℤ: Type
ℤ
:=
Nat.castRingHom: (α : Type ?u.55) → [inst : NonAssocSemiring α] → ℕ →+* α
Nat.castRingHom
ℤ: Type
ℤ
#align int.of_nat_hom
Int.ofNatHom: ℕ →+* ℤ
Int.ofNatHom
-- Porting note: no need to be `@[simp]`, as `Nat.cast_pos` handles this. -- @[simp] theorem
coe_nat_pos: ∀ {n : ℕ}, 0 < ↑n ↔ 0 < n
coe_nat_pos
{n :
ℕ: Type
ℕ
} : (
0: ?m.522
0
:
ℤ: Type
ℤ
) < n ↔
0: ?m.611
0
< n :=
Nat.cast_pos: ∀ {α : Type ?u.641} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] {n : ℕ}, 0 < ↑n ↔ 0 < n
Nat.cast_pos
#align int.coe_nat_pos
Int.coe_nat_pos: ∀ {n : ℕ}, 0 < ↑n ↔ 0 < n
Int.coe_nat_pos
theorem
coe_nat_succ_pos: ∀ (n : ℕ), 0 < ↑(Nat.succ n)
coe_nat_succ_pos
(n :
ℕ: Type
ℕ
) :
0: ?m.773
0
< (n.
succ: ℕ → ℕ
succ
:
ℤ: Type
ℤ
) :=
Int.coe_nat_pos: ∀ {n : ℕ}, 0 < ↑n ↔ 0 < n
Int.coe_nat_pos
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
(
succ_pos: ∀ (n : ℕ), 0 < Nat.succ n
succ_pos
n) #align int.coe_nat_succ_pos
Int.coe_nat_succ_pos: ∀ (n : ℕ), 0 < ↑(Nat.succ n)
Int.coe_nat_succ_pos
lemma
toNat_lt': ∀ {a : ℤ} {b : ℕ}, b ≠ 0 → (toNat a < b ↔ a < ↑b)
toNat_lt'
{a :
ℤ: Type
ℤ
} {b :
ℕ: Type
ℕ
} (
hb: b ≠ 0
hb
: b ≠
0: ?m.884
0
) : a.
toNat: ℤ → ℕ
toNat
< b ↔ a < b :=

Goals accomplished! 🐙
F: Type ?u.865

ι: Type ?u.868

α: Type ?u.871

β: Type ?u.874

a: ℤ

b: ℕ

hb: b ≠ 0


toNat a < b ↔ a < ↑b
F: Type ?u.865

ι: Type ?u.868

α: Type ?u.871

β: Type ?u.874

a: ℤ

b: ℕ

hb: b ≠ 0


toNat a < b ↔ a < ↑b
F: Type ?u.865

ι: Type ?u.868

α: Type ?u.871

β: Type ?u.874

a: ℤ

b: ℕ

hb: b ≠ 0


toNat a < b ↔ toNat a < toNat ↑b
F: Type ?u.865

ι: Type ?u.868

α: Type ?u.871

β: Type ?u.874

a: ℤ

b: ℕ

hb: b ≠ 0


0 < ↑b
F: Type ?u.865

ι: Type ?u.868

α: Type ?u.871

β: Type ?u.874

a: ℤ

b: ℕ

hb: b ≠ 0


toNat a < b ↔ a < ↑b
F: Type ?u.865

ι: Type ?u.868

α: Type ?u.871

β: Type ?u.874

a: ℤ

b: ℕ

hb: b ≠ 0


toNat a < b ↔ toNat a < b
F: Type ?u.865

ι: Type ?u.868

α: Type ?u.871

β: Type ?u.874

a: ℤ

b: ℕ

hb: b ≠ 0


0 < ↑b
F: Type ?u.865

ι: Type ?u.868

α: Type ?u.871

β: Type ?u.874

a: ℤ

b: ℕ

hb: b ≠ 0


0 < ↑b
F: Type ?u.865

ι: Type ?u.868

α: Type ?u.871

β: Type ?u.874

a: ℤ

b: ℕ

hb: b ≠ 0


0 < ↑b
F: Type ?u.865

ι: Type ?u.868

α: Type ?u.871

β: Type ?u.874

a: ℤ

b: ℕ

hb: b ≠ 0


toNat a < b ↔ a < ↑b

Goals accomplished! 🐙
#align int.to_nat_lt
Int.toNat_lt': ∀ {a : ℤ} {b : ℕ}, b ≠ 0 → (toNat a < b ↔ a < ↑b)
Int.toNat_lt'
lemma
natMod_lt: ∀ {a : ℤ} {b : ℕ}, b ≠ 0 → natMod a ↑b < b
natMod_lt
{a :
ℤ: Type
ℤ
} {b :
ℕ: Type
ℕ
} (
hb: b ≠ 0
hb
: b ≠
0: ?m.1129
0
) : a.
natMod: ℤ → ℤ → ℕ
natMod
b < b := (
toNat_lt': ∀ {a : ℤ} {b : ℕ}, b ≠ 0 → (toNat a < b ↔ a < ↑b)
toNat_lt'
hb: b ≠ 0
hb
).
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
$
emod_lt_of_pos: ∀ (a : ℤ) {b : ℤ}, 0 < b → a % b < b
emod_lt_of_pos
_ $
coe_nat_pos: ∀ {n : ℕ}, 0 < ↑n ↔ 0 < n
coe_nat_pos
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
hb: b ≠ 0
hb
.
bot_lt: ∀ {α : Type ?u.1225} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a ≠ ⊥ → ⊥ < a
bot_lt
#align int.nat_mod_lt
Int.natMod_lt: ∀ {a : ℤ} {b : ℕ}, b ≠ 0 → natMod a ↑b < b
Int.natMod_lt
section cast @[simp, norm_cast] theorem
cast_mul: ∀ {α : Type u_1} [inst : NonAssocRing α] (m n : ℤ), ↑(m * n) = ↑m * ↑n
cast_mul
[
NonAssocRing: Type ?u.1336 → Type ?u.1336
NonAssocRing
α: Type ?u.1330
α
] : ∀
m: ?m.1340
m
n: ?m.1343
n
, ((
m: ?m.1340
m
*
n: ?m.1343
n
:
ℤ: Type
ℤ
) :
α: Type ?u.1330
α
) =
m: ?m.1340
m
*
n: ?m.1343
n
:= fun
m: ?m.1847
m
=>
Int.inductionOn': ∀ {C : ℤ → Sort ?u.1849} (z b : ℤ), C b → (∀ (k : ℤ), b ≤ k → C k → C (k + 1)) → (∀ (k : ℤ), k ≤ b → C k → C (k - 1)) → C z
Int.inductionOn'
m: ?m.1847
m
0: ?m.1899
0
(

Goals accomplished! 🐙
F: Type ?u.1324

ι: Type ?u.1327

α: Type u_1

β: Type ?u.1333

inst✝: NonAssocRing α

m: ℤ


∀ (n : ℤ), ↑(0 * n) = ↑0 * ↑n

Goals accomplished! 🐙
) (fun
k: ?m.1911
k
_: ?m.1914
_
ih: ?m.1917
ih
n: ?m.1921
n
=>

Goals accomplished! 🐙
F: Type ?u.1324

ι: Type ?u.1327

α: Type u_1

β: Type ?u.1333

inst✝: NonAssocRing α

m, k: ℤ

x✝: 0 ≤ k

ih: ∀ (n : ℤ), ↑(k * n) = ↑k * ↑n

n: ℤ


↑((k + 1) * n) = ↑(k + 1) * ↑n

Goals accomplished! 🐙
) fun
k: ?m.1930
k
_: ?m.1933
_
ih: ?m.1936
ih
n: ?m.1940
n
=>

Goals accomplished! 🐙
F: Type ?u.1324

ι: Type ?u.1327

α: Type u_1

β: Type ?u.1333

inst✝: NonAssocRing α

m, k: ℤ

x✝: k ≤ 0

ih: ∀ (n : ℤ), ↑(k * n) = ↑k * ↑n

n: ℤ


↑((k - 1) * n) = ↑(k - 1) * ↑n

Goals accomplished! 🐙
#align int.cast_mul
Int.cast_mulₓ: ∀ {α : Type u_1} [inst : NonAssocRing α] (m n : ℤ), ↑(m * n) = ↑m * ↑n
Int.cast_mulₓ
-- dubious translation, type involves HasLiftT @[simp, norm_cast] theorem
cast_ite: ∀ {α : Type u_1} [inst : AddGroupWithOne α] (P : Prop) [inst_1 : Decidable P] (m n : ℤ), ↑(if P then m else n) = if P then ↑m else ↑n
cast_ite
[
AddGroupWithOne: Type ?u.3569 → Type ?u.3569
AddGroupWithOne
α: Type ?u.3563
α
] (
P: Prop
P
:
Prop: Type
Prop
) [
Decidable: Prop → Type
Decidable
P: Prop
P
] (m n :
ℤ: Type
ℤ
) : ((
ite: {α : Sort ?u.3583} → (c : Prop) → [h : Decidable c] → α → α → α
ite
P: Prop
P
m n :
ℤ: Type
ℤ
) :
α: Type ?u.3563
α
) =
ite: {α : Sort ?u.3701} → (c : Prop) → [h : Decidable c] → α → α → α
ite
P: Prop
P
(m :
α: Type ?u.3563
α
) (n :
α: Type ?u.3563
α
) :=
apply_ite: ∀ {α : Sort ?u.3881} {β : Sort ?u.3882} (f : α → β) (P : Prop) [inst : Decidable P] (x y : α), f (if P then x else y) = if P then f x else f y
apply_ite
_: ?m.3883 → ?m.3884
_
_: Prop
_
_: ?m.3883
_
_: ?m.3883
_
#align int.cast_ite
Int.cast_ite: ∀ {α : Type u_1} [inst : AddGroupWithOne α] (P : Prop) [inst_1 : Decidable P] (m n : ℤ), ↑(if P then m else n) = if P then ↑m else ↑n
Int.cast_ite
/-- `coe : ℤ → α` as an `AddMonoidHom`. -/ def
castAddHom: (α : Type u_1) → [inst : AddGroupWithOne α] → ℤ →+ α
castAddHom
(
α: Type ?u.4179
α
:
Type _: Type (?u.4179+1)
Type _
) [
AddGroupWithOne: Type ?u.4182 → Type ?u.4182
AddGroupWithOne
α: Type ?u.4179
α
] :
ℤ: Type
ℤ
→+
α: Type ?u.4179
α
where toFun :=
Int.cast: {R : Type ?u.4692} → [inst : IntCast R] → ℤ → R
Int.cast
map_zero' :=
cast_zero: ∀ {R : Type ?u.4768} [inst : AddGroupWithOne R], ↑0 = 0
cast_zero
map_add' :=
cast_add: ∀ {R : Type ?u.4785} [inst : AddGroupWithOne R] (m n : ℤ), ↑(m + n) = ↑m + ↑n
cast_add
#align int.cast_add_hom
Int.castAddHom: (α : Type u_1) → [inst : AddGroupWithOne α] → ℤ →+ α
Int.castAddHom
@[simp] theorem
coe_castAddHom: ∀ {α : Type u_1} [inst : AddGroupWithOne α], ↑(castAddHom α) = fun x => ↑x
coe_castAddHom
[
AddGroupWithOne: Type ?u.4896 → Type ?u.4896
AddGroupWithOne
α: Type ?u.4890
α
] : ⇑(
castAddHom: (α : Type ?u.4900) → [inst : AddGroupWithOne α] → ℤ →+ α
castAddHom
α: Type ?u.4890
α
) = fun x :
ℤ: Type
ℤ
=> (x :
α: Type ?u.4890
α
) :=
rfl: ∀ {α : Sort ?u.5811} {a : α}, a = a
rfl
#align int.coe_cast_add_hom
Int.coe_castAddHom: ∀ {α : Type u_1} [inst : AddGroupWithOne α], ↑(castAddHom α) = fun x => ↑x
Int.coe_castAddHom
/-- `coe : ℤ → α` as a `RingHom`. -/ def
castRingHom: (α : Type u_1) → [inst : NonAssocRing α] → ℤ →+* α
castRingHom
(
α: Type ?u.5857
α
:
Type _: Type (?u.5857+1)
Type _
) [
NonAssocRing: Type ?u.5860 → Type ?u.5860
NonAssocRing
α: Type ?u.5857
α
] :
ℤ: Type
ℤ
→+*
α: Type ?u.5857
α
where toFun :=
Int.cast: {R : Type ?u.6483} → [inst : IntCast R] → ℤ → R
Int.cast
map_zero' :=
cast_zero: ∀ {R : Type ?u.6634} [inst : AddGroupWithOne R], ↑0 = 0
cast_zero
map_add' :=
cast_add: ∀ {R : Type ?u.6645} [inst : AddGroupWithOne R] (m n : ℤ), ↑(m + n) = ↑m + ↑n
cast_add
map_one' :=
cast_one: ∀ {R : Type ?u.6545} [inst : AddGroupWithOne R], ↑1 = 1
cast_one
map_mul' :=
cast_mul: ∀ {α : Type ?u.6612} [inst : NonAssocRing α] (m n : ℤ), ↑(m * n) = ↑m * ↑n
cast_mul
#align int.cast_ring_hom
Int.castRingHom: (α : Type u_1) → [inst : NonAssocRing α] → ℤ →+* α
Int.castRingHom
@[simp] theorem
coe_castRingHom: ∀ {α : Type u_1} [inst : NonAssocRing α], ↑(castRingHom α) = fun x => ↑x
coe_castRingHom
[
NonAssocRing: Type ?u.6730 → Type ?u.6730
NonAssocRing
α: Type ?u.6724
α
] : ⇑(
castRingHom: (α : Type ?u.6734) → [inst : NonAssocRing α] → ℤ →+* α
castRingHom
α: Type ?u.6724
α
) = fun x :
ℤ: Type
ℤ
=> (x :
α: Type ?u.6724
α
) :=
rfl: ∀ {α : Sort ?u.7221} {a : α}, a = a
rfl
#align int.coe_cast_ring_hom
Int.coe_castRingHom: ∀ {α : Type u_1} [inst : NonAssocRing α], ↑(castRingHom α) = fun x => ↑x
Int.coe_castRingHom
theorem
cast_commute: ∀ {α : Type u_1} [inst : NonAssocRing α] (m : ℤ) (x : α), Commute (↑m) x
cast_commute
[
NonAssocRing: Type ?u.7267 → Type ?u.7267
NonAssocRing
α: Type ?u.7261
α
] : ∀ (m :
ℤ: Type
ℤ
) (
x: α
x
:
α: Type ?u.7261
α
),
Commute: {S : Type ?u.7275} → [inst : Mul S] → S → S → Prop
Commute
(↑m)
x: α
x
| (n : ℕ),
x: α
x
=>

Goals accomplished! 🐙
F: Type ?u.7255

ι: Type ?u.7258

α: Type u_1

β: Type ?u.7264

inst✝: NonAssocRing α

n: ℕ

x: α


Commute (↑↑n) x

Goals accomplished! 🐙
| -[n+1],
x: α
x
=>

Goals accomplished! 🐙
F: Type ?u.7255

ι: Type ?u.7258

α: Type u_1

β: Type ?u.7264

inst✝: NonAssocRing α

n: ℕ

x: α


Commute (↑-[n+1]) x

Goals accomplished! 🐙
#align int.cast_commute
Int.cast_commute: ∀ {α : Type u_1} [inst : NonAssocRing α] (m : ℤ) (x : α), Commute (↑m) x
Int.cast_commute
theorem
cast_comm: ∀ [inst : NonAssocRing α] (m : ℤ) (x : α), ↑m * x = x * ↑m
cast_comm
[
NonAssocRing: Type ?u.8746 → Type ?u.8746
NonAssocRing
α: Type ?u.8740
α
] (m :
ℤ: Type
ℤ
) (
x: α
x
:
α: Type ?u.8740
α
) : (m :
α: Type ?u.8740
α
) *
x: α
x
=
x: α
x
* m := (
cast_commute: ∀ {α : Type ?u.9032} [inst : NonAssocRing α] (m : ℤ) (x : α), Commute (↑m) x
cast_commute
m
x: α
x
).
eq: ∀ {S : Type ?u.9038} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq
#align int.cast_comm
Int.cast_comm: ∀ {α : Type u_1} [inst : NonAssocRing α] (m : ℤ) (x : α), ↑m * x = x * ↑m
Int.cast_comm
theorem
commute_cast: ∀ [inst : NonAssocRing α] (x : α) (m : ℤ), Commute x ↑m
commute_cast
[
NonAssocRing: Type ?u.9094 → Type ?u.9094
NonAssocRing
α: Type ?u.9088
α
] (
x: α
x
:
α: Type ?u.9088
α
) (m :
ℤ: Type
ℤ
) :
Commute: {S : Type ?u.9101} → [inst : Mul S] → S → S → Prop
Commute
x: α
x
m := (m.
cast_commute: ∀ {α : Type ?u.9251} [inst : NonAssocRing α] (m : ℤ) (x : α), Commute (↑m) x
cast_commute
x: α
x
).
symm: ∀ {S : Type ?u.9261} [inst : Mul S] {a b : S}, Commute a b → Commute b a
symm
#align int.commute_cast
Int.commute_cast: ∀ {α : Type u_1} [inst : NonAssocRing α] (x : α) (m : ℤ), Commute x ↑m
Int.commute_cast
theorem
cast_mono: ∀ {α : Type u_1} [inst : OrderedRing α], Monotone fun x => ↑x
cast_mono
[
OrderedRing: Type ?u.9314 → Type ?u.9314
OrderedRing
α: Type ?u.9308
α
] :
Monotone: {α : Type ?u.9318} → {β : Type ?u.9317} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone
(fun x :
ℤ: Type
ℤ
=> (x :
α: Type ?u.9308
α
)) :=

Goals accomplished! 🐙
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α


Monotone fun x => ↑x
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n


(fun x => ↑x) m ≤ (fun x => ↑x) n
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α


Monotone fun x => ↑x
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n


(fun x => ↑x) m ≤ (fun x => ↑x) n
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h✝: m ≤ n

h: 0 ≤ n - m


(fun x => ↑x) m ≤ (fun x => ↑x) n
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h✝: m ≤ n

h: 0 ≤ n - m


(fun x => ↑x) m ≤ (fun x => ↑x) n
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h✝: m ≤ n

h: 0 ≤ n - m


(fun x => ↑x) m ≤ (fun x => ↑x) n
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α


Monotone fun x => ↑x
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n

k: ℕ

hk: ↑k = n - m


intro
↑m ≤ ↑n
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α


Monotone fun x => ↑x
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n

k: ℕ

hk: ↑k = n - m


intro
↑m ≤ ↑n
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n

k: ℕ

hk: ↑k = n - m


intro
0 ≤ ↑n - ↑m
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n

k: ℕ

hk: ↑k = n - m


intro
↑m ≤ ↑n
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n

k: ℕ

hk: ↑k = n - m


intro
0 ≤ ↑(n - m)
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n

k: ℕ

hk: ↑k = n - m


intro
↑m ≤ ↑n
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n

k: ℕ

hk: ↑k = n - m


intro
0 ≤ ↑↑k
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n

k: ℕ

hk: ↑k = n - m


intro
↑m ≤ ↑n
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n

k: ℕ

hk: ↑k = n - m


intro
0 ≤ ↑k
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α

m, n: ℤ

h: m ≤ n

k: ℕ

hk: ↑k = n - m


intro
0 ≤ ↑k
F: Type ?u.9302

ι: Type ?u.9305

α: Type u_1

β: Type ?u.9311

inst✝: OrderedRing α


Monotone fun x => ↑x

Goals accomplished! 🐙
#align int.cast_mono
Int.cast_mono: ∀ {α : Type u_1} [inst : OrderedRing α], Monotone fun x => ↑x
Int.cast_mono
@[simp] theorem
cast_nonneg: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α] {n : ℤ}, 0 ≤ ↑n ↔ 0 ≤ n
cast_nonneg
[
OrderedRing: Type ?u.10845 → Type ?u.10845
OrderedRing
α: Type ?u.10839
α
] [
Nontrivial: Type ?u.10848 → Prop
Nontrivial
α: Type ?u.10839
α
] : ∀ {n :
ℤ: Type
ℤ
}, (
0: ?m.10857
0
:
α: Type ?u.10839
α
) ≤ n ↔
0: ?m.11220
0
≤ n | (n : ℕ) =>

Goals accomplished! 🐙
F: Type ?u.10833

ι: Type ?u.10836

α: Type u_1

β: Type ?u.10842

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℕ


0 ≤ ↑↑n ↔ 0 ≤ ↑n

Goals accomplished! 🐙
| -[n+1] =>

Goals accomplished! 🐙
F: Type ?u.10833

ι: Type ?u.10836

α: Type u_1

β: Type ?u.10842

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℕ


F: Type ?u.10833

ι: Type ?u.10836

α: Type u_1

β: Type ?u.10842

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℕ



Goals accomplished! 🐙
F: Type ?u.10833

ι: Type ?u.10836

α: Type u_1

β: Type ?u.10842

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℕ


-↑n ≤ 0

Goals accomplished! 🐙
F: Type ?u.10833

ι: Type ?u.10836

α: Type u_1

β: Type ?u.10842

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℕ

this: -↑n < 1


F: Type ?u.10833

ι: Type ?u.10836

α: Type u_1

β: Type ?u.10842

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℕ



Goals accomplished! 🐙
#align int.cast_nonneg
Int.cast_nonneg: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α] {n : ℤ}, 0 ≤ ↑n ↔ 0 ≤ n
Int.cast_nonneg
@[simp, norm_cast] theorem
cast_le: ∀ [inst : OrderedRing α] [inst_1 : Nontrivial α] {m n : ℤ}, ↑m ≤ ↑n ↔ m ≤ n
cast_le
[
OrderedRing: Type ?u.15861 → Type ?u.15861
OrderedRing
α: Type ?u.15855
α
] [
Nontrivial: Type ?u.15864 → Prop
Nontrivial
α: Type ?u.15855
α
] {m n :
ℤ: Type
ℤ
} : (m :
α: Type ?u.15855
α
) ≤ n ↔ m ≤ n :=

Goals accomplished! 🐙
F: Type ?u.15849

ι: Type ?u.15852

α: Type u_1

β: Type ?u.15858

inst✝¹: OrderedRing α

inst✝: Nontrivial α

m, n: ℤ


↑m ≤ ↑n ↔ m ≤ n
F: Type ?u.15849

ι: Type ?u.15852

α: Type u_1

β: Type ?u.15858

inst✝¹: OrderedRing α

inst✝: Nontrivial α

m, n: ℤ


↑m ≤ ↑n ↔ m ≤ n
F: Type ?u.15849

ι: Type ?u.15852

α: Type u_1

β: Type ?u.15858

inst✝¹: OrderedRing α

inst✝: Nontrivial α

m, n: ℤ


0 ≤ ↑n - ↑m ↔ m ≤ n
F: Type ?u.15849

ι: Type ?u.15852

α: Type u_1

β: Type ?u.15858

inst✝¹: OrderedRing α

inst✝: Nontrivial α

m, n: ℤ


↑m ≤ ↑n ↔ m ≤ n
F: Type ?u.15849

ι: Type ?u.15852

α: Type u_1

β: Type ?u.15858

inst✝¹: OrderedRing α

inst✝: Nontrivial α

m, n: ℤ


0 ≤ ↑(n - m) ↔ m ≤ n
F: Type ?u.15849

ι: Type ?u.15852

α: Type u_1

β: Type ?u.15858

inst✝¹: OrderedRing α

inst✝: Nontrivial α

m, n: ℤ


↑m ≤ ↑n ↔ m ≤ n
F: Type ?u.15849

ι: Type ?u.15852

α: Type u_1

β: Type ?u.15858

inst✝¹: OrderedRing α

inst✝: Nontrivial α

m, n: ℤ


0 ≤ n - m ↔ m ≤ n
F: Type ?u.15849

ι: Type ?u.15852

α: Type u_1

β: Type ?u.15858

inst✝¹: OrderedRing α

inst✝: Nontrivial α

m, n: ℤ


↑m ≤ ↑n ↔ m ≤ n
F: Type ?u.15849

ι: Type ?u.15852

α: Type u_1

β: Type ?u.15858

inst✝¹: OrderedRing α

inst✝: Nontrivial α

m, n: ℤ



Goals accomplished! 🐙
#align int.cast_le
Int.cast_le: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α] {m n : ℤ}, ↑m ≤ ↑n ↔ m ≤ n
Int.cast_le
theorem
cast_strictMono: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α], StrictMono fun x => ↑x
cast_strictMono
[
OrderedRing: Type ?u.17074 → Type ?u.17074
OrderedRing
α: Type ?u.17068
α
] [
Nontrivial: Type ?u.17077 → Prop
Nontrivial
α: Type ?u.17068
α
] :
StrictMono: {α : Type ?u.17081} → {β : Type ?u.17080} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
StrictMono
(fun x :
ℤ: Type
ℤ
=> (x :
α: Type ?u.17068
α
)) :=
strictMono_of_le_iff_le: ∀ {α : Type ?u.17310} {β : Type ?u.17309} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, (∀ (x y : α), x ≤ y ↔ f x ≤ f y) → StrictMono f
strictMono_of_le_iff_le
fun
_: ?m.17361
_
_: ?m.17364
_
=>
cast_le: ∀ {α : Type ?u.17366} [inst : OrderedRing α] [inst_1 : Nontrivial α] {m n : ℤ}, ↑m ≤ ↑n ↔ m ≤ n
cast_le
.
symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm
#align int.cast_strict_mono
Int.cast_strictMono: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α], StrictMono fun x => ↑x
Int.cast_strictMono
@[simp, norm_cast] theorem
cast_lt: ∀ [inst : OrderedRing α] [inst_1 : Nontrivial α] {m n : ℤ}, ↑m < ↑n ↔ m < n
cast_lt
[
OrderedRing: Type ?u.17585 → Type ?u.17585
OrderedRing
α: Type ?u.17579
α
] [
Nontrivial: Type ?u.17588 → Prop
Nontrivial
α: Type ?u.17579
α
] {m n :
ℤ: Type
ℤ
} : (m :
α: Type ?u.17579
α
) < n ↔ m < n :=
cast_strictMono: ∀ {α : Type ?u.17865} [inst : OrderedRing α] [inst_1 : Nontrivial α], StrictMono fun x => ↑x
cast_strictMono
.
lt_iff_lt: ∀ {α : Type ?u.17902} {β : Type ?u.17901} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β}, StrictMono f → ∀ {a b : α}, f a < f b ↔ a < b
lt_iff_lt
#align int.cast_lt
Int.cast_lt: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α] {m n : ℤ}, ↑m < ↑n ↔ m < n
Int.cast_lt
@[simp] theorem
cast_nonpos: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α] {n : ℤ}, ↑n ≤ 0 ↔ n ≤ 0
cast_nonpos
[
OrderedRing: Type ?u.18196 → Type ?u.18196
OrderedRing
α: Type ?u.18190
α
] [
Nontrivial: Type ?u.18199 → Prop
Nontrivial
α: Type ?u.18190
α
] {n :
ℤ: Type
ℤ
} : (n :
α: Type ?u.18190
α
) ≤
0: ?m.18279
0
↔ n ≤
0: ?m.18530
0
:=

Goals accomplished! 🐙
F: Type ?u.18184

ι: Type ?u.18187

α: Type u_1

β: Type ?u.18193

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


↑n ≤ 0 ↔ n ≤ 0
F: Type ?u.18184

ι: Type ?u.18187

α: Type u_1

β: Type ?u.18193

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


↑n ≤ 0 ↔ n ≤ 0
F: Type ?u.18184

ι: Type ?u.18187

α: Type u_1

β: Type ?u.18193

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


↑n ≤ ↑0 ↔ n ≤ 0
F: Type ?u.18184

ι: Type ?u.18187

α: Type u_1

β: Type ?u.18193

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


↑n ≤ 0 ↔ n ≤ 0
F: Type ?u.18184

ι: Type ?u.18187

α: Type u_1

β: Type ?u.18193

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ



Goals accomplished! 🐙
#align int.cast_nonpos
Int.cast_nonpos: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α] {n : ℤ}, ↑n ≤ 0 ↔ n ≤ 0
Int.cast_nonpos
@[simp] theorem
cast_pos: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α] {n : ℤ}, 0 < ↑n ↔ 0 < n
cast_pos
[
OrderedRing: Type ?u.18787 → Type ?u.18787
OrderedRing
α: Type ?u.18781
α
] [
Nontrivial: Type ?u.18790 → Prop
Nontrivial
α: Type ?u.18781
α
] {n :
ℤ: Type
ℤ
} : (
0: ?m.18798
0
:
α: Type ?u.18781
α
) < n ↔
0: ?m.19161
0
< n :=

Goals accomplished! 🐙
F: Type ?u.18775

ι: Type ?u.18778

α: Type u_1

β: Type ?u.18784

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


0 < ↑n ↔ 0 < n
F: Type ?u.18775

ι: Type ?u.18778

α: Type u_1

β: Type ?u.18784

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


0 < ↑n ↔ 0 < n
F: Type ?u.18775

ι: Type ?u.18778

α: Type u_1

β: Type ?u.18784

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


↑0 < ↑n ↔ 0 < n
F: Type ?u.18775

ι: Type ?u.18778

α: Type u_1

β: Type ?u.18784

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


0 < ↑n ↔ 0 < n
F: Type ?u.18775

ι: Type ?u.18778

α: Type u_1

β: Type ?u.18784

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


0 < n ↔ 0 < n

Goals accomplished! 🐙
#align int.cast_pos
Int.cast_pos: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α] {n : ℤ}, 0 < ↑n ↔ 0 < n
Int.cast_pos
@[simp] theorem
cast_lt_zero: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α] {n : ℤ}, ↑n < 0 ↔ n < 0
cast_lt_zero
[
OrderedRing: Type ?u.19426 → Type ?u.19426
OrderedRing
α: Type ?u.19420
α
] [
Nontrivial: Type ?u.19429 → Prop
Nontrivial
α: Type ?u.19420
α
] {n :
ℤ: Type
ℤ
} : (n :
α: Type ?u.19420
α
) <
0: ?m.19509
0
↔ n <
0: ?m.19760
0
:=

Goals accomplished! 🐙
F: Type ?u.19414

ι: Type ?u.19417

α: Type u_1

β: Type ?u.19423

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


↑n < 0 ↔ n < 0
F: Type ?u.19414

ι: Type ?u.19417

α: Type u_1

β: Type ?u.19423

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


↑n < 0 ↔ n < 0
F: Type ?u.19414

ι: Type ?u.19417

α: Type u_1

β: Type ?u.19423

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


↑n < ↑0 ↔ n < 0
F: Type ?u.19414

ι: Type ?u.19417

α: Type u_1

β: Type ?u.19423

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


↑n < 0 ↔ n < 0
F: Type ?u.19414

ι: Type ?u.19417

α: Type u_1

β: Type ?u.19423

inst✝¹: OrderedRing α

inst✝: Nontrivial α

n: ℤ


n < 0 ↔ n < 0

Goals accomplished! 🐙
#align int.cast_lt_zero
Int.cast_lt_zero: ∀ {α : Type u_1} [inst : OrderedRing α] [inst_1 : Nontrivial α] {n : ℤ}, ↑n < 0 ↔ n < 0
Int.cast_lt_zero
section LinearOrderedRing variable [
LinearOrderedRing: Type ?u.20902 → Type ?u.20902
LinearOrderedRing
α: Type ?u.26505
α
] {a b :
ℤ: Type
ℤ
} (n :
ℤ: Type
ℤ
) @[simp, norm_cast] theorem
cast_min: ↑(min a b) = min ↑a ↑b
cast_min
: (↑(
min: {α : Type ?u.20049} → [self : Min α] → α → α → α
min
a b) :
α: Type ?u.20032
α
) =
min: {α : Type ?u.20121} → [self : Min α] → α → α → α
min
(a :
α: Type ?u.20032
α
) (b :
α: Type ?u.20032
α
) :=
Monotone.map_min: ∀ {α : Type ?u.20227} {β : Type ?u.20226} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α}, Monotone f → f (min a b) = min (f a) (f b)
Monotone.map_min
cast_mono: ∀ {α : Type ?u.20306} [inst : OrderedRing α], Monotone fun x => ↑x
cast_mono
#align int.cast_min
Int.cast_min: ∀ {α : Type u_1} [inst : LinearOrderedRing α] {a b : ℤ}, ↑(min a b) = min ↑a ↑b
Int.cast_min
@[simp, norm_cast] theorem
cast_max: ∀ {α : Type u_1} [inst : LinearOrderedRing α] {a b : ℤ}, ↑(max a b) = max ↑a ↑b
cast_max
: (↑(
max: {α : Type ?u.20481} → [self : Max α] → α → α → α
max
a b) :
α: Type ?u.20464
α
) =
max: {α : Type ?u.20553} → [self : Max α] → α → α → α
max
(a :
α: Type ?u.20464
α
) (b :
α: Type ?u.20464
α
) :=
Monotone.map_max: ∀ {α : Type ?u.20659} {β : Type ?u.20658} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α}, Monotone f → f (max a b) = max (f a) (f b)
Monotone.map_max
cast_mono: ∀ {α : Type ?u.20738} [inst : OrderedRing α], Monotone fun x => ↑x
cast_mono
#align int.cast_max
Int.cast_max: ∀ {α : Type u_1} [inst : LinearOrderedRing α] {a b : ℤ}, ↑(max a b) = max ↑a ↑b
Int.cast_max
@[simp, norm_cast] theorem
cast_abs: ↑(abs a) = abs ↑a
cast_abs
: ((|a| :
ℤ: Type
ℤ
) :
α: Type ?u.20896
α
) = |(a :
α: Type ?u.20896
α
)| :=

Goals accomplished! 🐙
F: Type ?u.20890

ι: Type ?u.20893

α: Type u_1

β: Type ?u.20899

inst✝: LinearOrderedRing α

a, b, n: ℤ


↑(abs a) = abs ↑a

Goals accomplished! 🐙
#align int.cast_abs
Int.cast_abs: ∀ {α : Type u_1} [inst : LinearOrderedRing α] {a : ℤ}, ↑(abs a) = abs ↑a
Int.cast_abs
theorem
cast_one_le_of_pos: ∀ {α : Type u_1} [inst : LinearOrderedRing α] {a : ℤ}, 0 < a → 1 ≤ ↑a
cast_one_le_of_pos
(
h: 0 < a
h
:
0: ?m.26522
0
< a) : (
1: ?m.26560
1
:
α: Type ?u.26505
α
) ≤ a :=

Goals accomplished! 🐙
F: Type ?u.26499

ι: Type ?u.26502

α: Type u_1

β: Type ?u.26508

inst✝: LinearOrderedRing α

a, b, n: ℤ

h: 0 < a


1 ≤ ↑a

Goals accomplished! 🐙
#align int.cast_one_le_of_pos
Int.cast_one_le_of_pos: ∀ {α : Type u_1} [inst : LinearOrderedRing α] {a : ℤ}, 0 < a → 1 ≤ ↑a
Int.cast_one_le_of_pos
theorem
cast_le_neg_one_of_neg: ∀ {α : Type u_1} [inst : LinearOrderedRing α] {a : ℤ}, a < 0 → ↑a ≤ -1
cast_le_neg_one_of_neg
(
h: a < 0
h
: a <
0: ?m.27429
0
) : (a :
α: Type ?u.27412
α
) ≤ -
1: ?m.27520
1
:=

Goals accomplished! 🐙
F: Type ?u.27406

ι: Type ?u.27409

α: Type u_1

β: Type ?u.27415

inst✝: LinearOrderedRing α

a, b, n: ℤ

h: a < 0


↑a ≤ -1
F: Type ?u.27406

ι: Type ?u.27409

α: Type u_1

β: Type ?u.27415

inst✝: LinearOrderedRing α

a, b, n: ℤ

h: a < 0


↑a ≤ -1
F: Type ?u.27406

ι: Type ?u.27409

α: Type u_1

β: Type ?u.27415

inst✝: LinearOrderedRing α

a, b, n: ℤ

h: a < 0


↑a ≤ -↑1
F: Type ?u.27406

ι: Type ?u.27409

α: Type u_1

β: Type ?u.27415

inst✝: LinearOrderedRing α

a, b, n: ℤ

h: a < 0


↑a ≤ -1
F: Type ?u.27406

ι: Type ?u.27409

α: Type u_1

β: Type ?u.27415

inst✝: LinearOrderedRing α

a, b, n: ℤ

h: a < 0


↑a ≤ ↑(-1)
F: Type ?u.27406

ι: Type ?u.27409

α: Type u_1

β: Type ?u.27415

inst✝: LinearOrderedRing α

a, b, n: ℤ

h: a < 0


↑a ≤ -1
F: Type ?u.27406

ι: Type ?u.27409

α: Type u_1

β: Type ?u.27415

inst✝: LinearOrderedRing α

a, b, n: ℤ

h: a < 0


F: Type ?u.27406

ι: Type ?u.27409

α: Type u_1

β: Type ?u.27415

inst✝: LinearOrderedRing α

a, b, n: ℤ

h: a < 0


F: Type ?u.27406

ι: Type ?u.27409

α: Type u_1

β: Type ?u.27415

inst✝: LinearOrderedRing α

a, b, n: ℤ

h: a < 0


↑a ≤ -1

Goals accomplished! 🐙
#align int.cast_le_neg_one_of_neg
Int.cast_le_neg_one_of_neg: ∀ {α : Type u_1} [inst : LinearOrderedRing α] {a : ℤ}, a < 0 → ↑a ≤ -1
Int.cast_le_neg_one_of_neg
variable (
α: ?m.28223
α
) {
n: ?m.28226
n
} theorem
cast_le_neg_one_or_one_le_cast_of_ne_zero: n ≠ 0 → ↑n ≤ -1 ∨ 1 ≤ ↑n
cast_le_neg_one_or_one_le_cast_of_ne_zero
(
hn: n ≠ 0
hn
: n ≠
0: ?m.28253
0
) : (n :
α: Type ?u.28235
α
) ≤ -
1: ?m.28326
1
∨
1: ?m.28460
1
≤ (n :
α: Type ?u.28235
α
) :=
hn: n ≠ 0
hn
.
lt_or_lt: ∀ {α : Type ?u.28485} [inst : LinearOrder α] {x y : α}, x ≠ y → x < y ∨ y < x
lt_or_lt
.
imp: ∀ {a c b d : Prop}, (a → c) → (b → d) → a ∨ b → c ∨ d
imp
cast_le_neg_one_of_neg: ∀ {α : Type ?u.28515} [inst : LinearOrderedRing α] {a : ℤ}, a < 0 → ↑a ≤ -1
cast_le_neg_one_of_neg
cast_one_le_of_pos: ∀ {α : Type ?u.28544} [inst : LinearOrderedRing α] {a : ℤ}, 0 < a → 1 ≤ ↑a
cast_one_le_of_pos
#align int.cast_le_neg_one_or_one_le_cast_of_ne_zero
Int.cast_le_neg_one_or_one_le_cast_of_ne_zero: ∀ (α : Type u_1) [inst : LinearOrderedRing α] {n : ℤ}, n ≠ 0 → ↑n ≤ -1 ∨ 1 ≤ ↑n
Int.cast_le_neg_one_or_one_le_cast_of_ne_zero
variable {
α: ?m.28607
α
} (
n: ?m.28610
n
) theorem
nneg_mul_add_sq_of_abs_le_one: ∀ {α : Type u_1} [inst : LinearOrderedRing α] (n : ℤ) {x : α}, abs x ≤ 1 → 0 ≤ ↑n * x + ↑n * ↑n
nneg_mul_add_sq_of_abs_le_one
{
x: α
x
:
α: Type ?u.28619
α
} (
hx: abs x ≤ 1
hx
: |
x: α
x
| ≤
1: ?m.28766
1
) : (
0: ?m.28878
0
:
α: Type ?u.28619
α
) ≤ n *
x: α
x
+ n * n :=

Goals accomplished! 🐙
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1


0 ≤ ↑n * x + ↑n * ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1


0 ≤ ↑n * x + ↑n * ↑n

Goals accomplished! 🐙
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hn: 0 < n


0 ≤ x + ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hn: 0 < n

this: -1 + 1 ≤ x + ↑n


0 ≤ x + ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hn: 0 < n


0 ≤ x + ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hn: 0 < n

this: -1 + 1 ≤ x + ↑n


0 ≤ x + ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hn: 0 < n

this: 0 ≤ x + ↑n


0 ≤ x + ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hn: 0 < n

this: 0 ≤ x + ↑n


0 ≤ x + ↑n

Goals accomplished! 🐙
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1


0 ≤ ↑n * x + ↑n * ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n


0 ≤ ↑n * x + ↑n * ↑n

Goals accomplished! 🐙
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hn: n < 0


x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hn: n < 0

this: x + ↑n ≤ 1 + -1


x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hn: n < 0


x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hn: n < 0

this: x + ↑n ≤ 1 + -1


x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hn: n < 0

this: x + ↑n ≤ 0


x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hn: n < 0

this: x + ↑n ≤ 0


x + ↑n ≤ 0

Goals accomplished! 🐙
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1


0 ≤ ↑n * x + ↑n * ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0


0 ≤ ↑n * x + ↑n * ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0


0 ≤ ↑n * (x + ↑n)
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0


0 ≤ ↑n * x + ↑n * ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0


0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0


0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1


0 ≤ ↑n * x + ↑n * ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: n < 0


inl
0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < 0 → 0 ≤ x + ↑0

hnx': 0 < 0 → x + ↑0 ≤ 0


inr.inl
0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: 0 < n


inr.inr
0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1


0 ≤ ↑n * x + ↑n * ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: n < 0


inl
0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: n < 0


inl
0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < 0 → 0 ≤ x + ↑0

hnx': 0 < 0 → x + ↑0 ≤ 0


inr.inl
0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: 0 < n


inr.inr
0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: n < 0


inl
0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Goals accomplished! 🐙
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: n < 0


↑n ≤ 0

Goals accomplished! 🐙

Goals accomplished! 🐙
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1


0 ≤ ↑n * x + ↑n * ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < 0 → 0 ≤ x + ↑0

hnx': 0 < 0 → x + ↑0 ≤ 0


inr.inl
0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < 0 → 0 ≤ x + ↑0

hnx': 0 < 0 → x + ↑0 ≤ 0


inr.inl
0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: 0 < n


inr.inr
0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Goals accomplished! 🐙
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1


0 ≤ ↑n * x + ↑n * ↑n
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: 0 < n


inr.inr
0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: 0 < n


inr.inr
0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: 0 < n


inr.inr
0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Goals accomplished! 🐙
F: Type ?u.28613

ι: Type ?u.28616

α: Type u_1

β: Type ?u.28622

inst✝: LinearOrderedRing α

a, b, n: ℤ

x: α

hx: abs x ≤ 1

hnx: 0 < n → 0 ≤ x + ↑n

hnx': n < 0 → x + ↑n ≤ 0

h: 0 < n


0 ≤ ↑n

Goals accomplished! 🐙

Goals accomplished! 🐙
#align int.nneg_mul_add_sq_of_abs_le_one
Int.nneg_mul_add_sq_of_abs_le_one: ∀ {α : Type u_1} [inst : LinearOrderedRing α] (n : ℤ) {x : α}, abs x ≤ 1 → 0 ≤ ↑n * x + ↑n * ↑n
Int.nneg_mul_add_sq_of_abs_le_one
theorem
cast_natAbs: ↑(natAbs n) = ↑(abs n)
cast_natAbs
: (n.
natAbs: ℤ → ℕ
natAbs
:
α: Type ?u.33875
α
) = |n| :=

Goals accomplished! 🐙
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b, n: ℤ


↑(natAbs n) = ↑(abs n)
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


ofNat
↑(natAbs (ofNat a✝)) = ↑(abs (ofNat a✝))
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑(natAbs -[a✝+1]) = ↑(abs -[a✝+1])
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b, n: ℤ


↑(natAbs n) = ↑(abs n)
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


ofNat
↑(natAbs (ofNat a✝)) = ↑(abs (ofNat a✝))
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


ofNat
↑(natAbs (ofNat a✝)) = ↑(abs (ofNat a✝))
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑(natAbs -[a✝+1]) = ↑(abs -[a✝+1])

Goals accomplished! 🐙
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b, n: ℤ


↑(natAbs n) = ↑(abs n)
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑(natAbs -[a✝+1]) = ↑(abs -[a✝+1])
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑(natAbs -[a✝+1]) = ↑(abs -[a✝+1])
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑(natAbs -[a✝+1]) = ↑(abs -[a✝+1])
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑(natAbs -[a✝+1]) = ↑↑(natAbs -[a✝+1])
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑(natAbs -[a✝+1]) = ↑(abs -[a✝+1])
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑(Nat.succ a✝) = ↑↑(Nat.succ a✝)
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑(natAbs -[a✝+1]) = ↑(abs -[a✝+1])
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑a✝ + 1 = ↑↑(Nat.succ a✝)
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑(natAbs -[a✝+1]) = ↑(abs -[a✝+1])
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑a✝ + 1 = ↑(Nat.succ a✝)
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑(natAbs -[a✝+1]) = ↑(abs -[a✝+1])
F: Type ?u.33869

ι: Type ?u.33872

α: Type u_1

β: Type ?u.33878

inst✝: LinearOrderedRing α

a, b: ℤ

a✝: ℕ


negSucc
↑a✝ + 1 = ↑a✝ + 1

Goals accomplished! 🐙
#align int.cast_nat_abs
Int.cast_natAbs: ∀ {α : Type u_1} [inst : LinearOrderedRing α] (n : ℤ), ↑(natAbs n) = ↑(abs n)
Int.cast_natAbs
end LinearOrderedRing theorem
coe_int_dvd: ∀ [inst : CommRing α] (m n : ℤ), m ∣ n → ↑m ∣ ↑n
coe_int_dvd
[
CommRing: Type ?u.34773 → Type ?u.34773
CommRing
α: Type ?u.34767
α
] (m n :
ℤ: Type
ℤ
) (
h: m ∣ n
h
: m ∣ n) : (m :
α: Type ?u.34767
α
) ∣ (n :
α: Type ?u.34767
α
) :=
RingHom.map_dvd: ∀ {α : Type ?u.34999} {β : Type ?u.35000} [inst : Semiring α] [inst_1 : Semiring β] (f : α →+* β) {a b : α}, a ∣ b → ↑f a ∣ ↑f b
RingHom.map_dvd
(
Int.castRingHom: (α : Type ?u.35005) → [inst : NonAssocRing α] → ℤ →+* α
Int.castRingHom
α: Type ?u.34767
α
)
h: m ∣ n
h
#align int.coe_int_dvd
Int.coe_int_dvd: ∀ {α : Type u_1} [inst : CommRing α] (m n : ℤ), m ∣ n → ↑m ∣ ↑n
Int.coe_int_dvd
end cast end Int open Int namespace AddMonoidHom variable {
A: Type ?u.35250
A
:
Type _: Type (?u.40874+1)
Type _
} /-- Two additive monoid homomorphisms `f`, `g` from `ℤ` to an additive monoid are equal if `f 1 = g 1`. -/ @[ext high] theorem
ext_int: ∀ [inst : AddMonoid A] {f g : ℤ →+ A}, ↑f 1 = ↑g 1 → f = g
ext_int
[
AddMonoid: Type ?u.35268 → Type ?u.35268
AddMonoid
A: Type ?u.35265
A
] {f g :
ℤ: Type
ℤ
→+
A: Type ?u.35265
A
} (
h1: ↑f 1 = ↑g 1
h1
: f
1: ?m.36088
1
= g
1: ?m.36860
1
) : f = g := have : f.
comp: {M : Type ?u.36877} → {N : Type ?u.36876} → {P : Type ?u.36875} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ P
comp
(
Int.ofNatHom: ℕ →+* ℤ
Int.ofNatHom
:
ℕ: Type
ℕ
→+
ℤ: Type
ℤ
) = g.
comp: {M : Type ?u.37157} → {N : Type ?u.37156} → {P : Type ?u.37155} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ P
comp
(
Int.ofNatHom: ℕ →+* ℤ
Int.ofNatHom
:
ℕ: Type
ℕ
→+
ℤ: Type
ℤ
) :=
ext_nat': ∀ {A : Type ?u.37178} {F : Type ?u.37179} [inst : AddMonoid A] [inst_1 : AddMonoidHomClass F ℕ A] (f g : F), ↑f 1 = ↑g 1 → f = g
ext_nat'
_: ?m.37181
_
_: ?m.37181
_
h1: ↑f 1 = ↑g 1
h1
have
this': ∀ (n : ℕ), ↑f ↑n = ↑g ↑n
this'
: ∀ n :
ℕ: Type
ℕ
, f n = g n :=
FunLike.ext_iff: ∀ {F : Sort ?u.38882} {α : Sort ?u.38884} {β : α → Sort ?u.38883} [i : FunLike F α β] {f g : F}, f = g ↔ ∀ (x : α), ↑f x = ↑g x
FunLike.ext_iff
.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1
this: comp f ↑ofNatHom = comp g ↑ofNatHom
this
ext: ∀ {M : Type ?u.39738} {N : Type ?u.39739} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] ⦃f g : M →+ N⦄, (∀ (x : M), ↑f x = ↑g x) → f = g
ext
fun
n: ?m.39775
n
=> match
n: ?m.39775
n
with | (n : ℕ) =>
this': ∀ (n : ℕ), ↑f ↑n = ↑g ↑n
this'
n |
.negSucc: ℕ → ℤ
.negSucc
n =>
eq_on_neg: ∀ {F : Type ?u.39851} {G : Type ?u.39852} {M : Type ?u.39853} [inst : AddGroup G] [inst_1 : AddMonoid M] [inst_2 : AddMonoidHomClass F G M] (f g : F) {x : G}, ↑f x = ↑g x → ↑f (-x) = ↑g (-x)
eq_on_neg
_: ?m.39854
_
_: ?m.39854
_
(
this': ∀ (n : ℕ), ↑f ↑n = ↑g ↑n
this'
<| n +
1: ?m.39993
1
) #align add_monoid_hom.ext_int
AddMonoidHom.ext_int: ∀ {A : Type u_1} [inst : AddMonoid A] {f g : ℤ →+ A}, ↑f 1 = ↑g 1 → f = g
AddMonoidHom.ext_int
variable [
AddGroupWithOne: Type ?u.40877 → Type ?u.40877
AddGroupWithOne
A: Type ?u.40892
A
] theorem
eq_int_castAddHom: ∀ (f : ℤ →+ A), ↑f 1 = 1 → f = castAddHom A
eq_int_castAddHom
(f :
ℤ: Type
ℤ
→+
A: Type ?u.40892
A
) (
h1: ↑f 1 = 1
h1
: f
1: ?m.41721
1
=
1: ?m.41732
1
) : f =
Int.castAddHom: (α : Type ?u.42003) → [inst : AddGroupWithOne α] → ℤ →+ α
Int.castAddHom
A: Type ?u.40892
A
:=
ext_int: ∀ {A : Type ?u.42012} [inst : AddMonoid A] {f g : ℤ →+ A}, ↑f 1 = ↑g 1 → f = g
ext_int
<|

Goals accomplished! 🐙
F: Type ?u.40880

ι: Type ?u.40883

α: Type ?u.40886

β: Type ?u.40889

A: Type u_1

inst✝: AddGroupWithOne A

f: ℤ →+ A

h1: ↑f 1 = 1


↑f 1 = ↑(castAddHom A) 1

Goals accomplished! 🐙
#align add_monoid_hom.eq_int_cast_hom
AddMonoidHom.eq_int_castAddHom: ∀ {A : Type u_1} [inst : AddGroupWithOne A] (f : ℤ →+ A), ↑f 1 = 1 → f = castAddHom A
AddMonoidHom.eq_int_castAddHom
end AddMonoidHom theorem
eq_intCast': ∀ [inst : AddGroupWithOne α] [inst_1 : AddMonoidHomClass F ℤ α] (f : F), ↑f 1 = 1 → ∀ (n : ℤ), ↑f n = ↑n
eq_intCast'
[
AddGroupWithOne: Type ?u.43207 → Type ?u.43207
AddGroupWithOne
α: Type ?u.43201
α
] [
AddMonoidHomClass: Type ?u.43212 → (M : outParam (Type ?u.43211)) → (N : outParam (Type ?u.43210)) → [inst : AddZeroClass M] → [inst : AddZeroClass N] → Type (max(max?u.43212?u.43211)?u.43210)
AddMonoidHomClass
F: Type ?u.43195
F
ℤ: Type
ℤ
α: Type ?u.43201
α
] (
f: F
f
:
F: Type ?u.43195
F
) (
h₁: ↑f 1 = 1
h₁
:
f: F
f
1: ?m.44027
1
=
1: ?m.44038
1
) : ∀ n :
ℤ: Type
ℤ
,
f: F
f
n = n :=
FunLike.ext_iff: ∀ {F : Sort ?u.45310} {α : Sort ?u.45312} {β : α → Sort ?u.45311} [i : FunLike F α β] {f g : F}, f = g ↔ ∀ (x : α), ↑f x = ↑g x
FunLike.ext_iff
.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1
<| (
f: F
f
:
ℤ: Type
ℤ
→+
α: Type ?u.43201
α
).
eq_int_castAddHom: ∀ {A : Type ?u.45521} [inst : AddGroupWithOne A] (f : ℤ →+ A), ↑f 1 = 1 → f = castAddHom A
eq_int_castAddHom
h₁: ↑f 1 = 1
h₁
#align eq_int_cast'
eq_intCast': ∀ {F : Type u_2} {α : Type u_1} [inst : AddGroupWithOne α] [inst_1 : AddMonoidHomClass F ℤ α] (f : F), ↑f 1 = 1 → ∀ (n : ℤ), ↑f n = ↑n
eq_intCast'
@[simp] theorem Int.castAddHom_int :
Int.castAddHom: (α : Type ?u.46909) → [inst : AddGroupWithOne α] → ℤ →+ α
Int.castAddHom
ℤ: Type
ℤ
=
AddMonoidHom.id: (M : Type ?u.46923) → [inst : AddZeroClass M] → M →+ M
AddMonoidHom.id
ℤ: Type
ℤ
:= ((
AddMonoidHom.id: (M : Type ?u.46951) → [inst : AddZeroClass M] → M →+ M
AddMonoidHom.id
ℤ: Type
ℤ
).
eq_int_castAddHom: ∀ {A : Type ?u.46953} [inst : AddGroupWithOne A] (f : ℤ →+ A), ↑f 1 = 1 → f = castAddHom A
eq_int_castAddHom
rfl: ∀ {α : Sort ?u.46962} {a : α}, a = a
rfl
).
symm: ∀ {α : Sort ?u.46969} {a b : α}, a = b → b = a
symm
#align int.cast_add_hom_int Int.castAddHom_int namespace MonoidHom variable {
M: Type ?u.47012
M
:
Type _: Type (?u.47012+1)
Type _
} [
Monoid: Type ?u.48769 → Type ?u.48769
Monoid
M: Type ?u.47012
M
] open Multiplicative @[ext] theorem
ext_mint: ∀ {M : Type u_1} [inst : Monoid M] {f g : Multiplicative ℤ →* M}, ↑f (↑ofAdd 1) = ↑g (↑ofAdd 1) → f = g
ext_mint
{f g :
Multiplicative: Type ?u.47267 → Type ?u.47267
Multiplicative
ℤ: Type
ℤ
→*
M: Type ?u.47012
M
} (
h1: ↑f (↑ofAdd 1) = ↑g (↑ofAdd 1)
h1
: f (
ofAdd: {α : Type ?u.47733} → α ≃ Multiplicative α
ofAdd
1: ?m.47812
1
) = g (
ofAdd: {α : Type ?u.48275} → α ≃ Multiplicative α
ofAdd
1: ?m.48354
1
)) : f = g :=
MonoidHom.toAdditive'': {α : Type ?u.48374} → {β : Type ?u.48373} → [inst : AddZeroClass α] → [inst_1 : MulOneClass β] → (Multiplicative α →* β) ≃ (α →+ Additive β)
MonoidHom.toAdditive''
.
injective: ∀ {α : Sort ?u.48405} {β : Sort ?u.48404} (e : α ≃ β), Function.Injective ↑e
injective
<|
AddMonoidHom.ext_int: ∀ {A : Type ?u.48429} [inst : AddMonoid A] {f g : ℤ →+ A}, ↑f 1 = ↑g 1 → f = g
AddMonoidHom.ext_int
<|
Additive.toMul: {α : Type ?u.48489} → Additive α ≃ α
Additive.toMul
.
injective: ∀ {α : Sort ?u.48492} {β : Sort ?u.48491} (e : α ≃ β), Function.Injective ↑e
injective
h1: ↑f (↑ofAdd 1) = ↑g (↑ofAdd 1)
h1
#align monoid_hom.ext_mint
MonoidHom.ext_mint: ∀ {M : Type u_1} [inst : Monoid M] {f g : Multiplicative ℤ →* M}, ↑f (↑ofAdd 1) = ↑g (↑ofAdd 1) → f = g
MonoidHom.ext_mint
/-- If two `MonoidHom`s agree on `-1` and the naturals then they are equal. -/ @[ext] theorem
ext_int: ∀ {M : Type u_1} [inst : Monoid M] {f g : ℤ →* M}, ↑f (-1) = ↑g (-1) → comp f ↑ofNatHom = comp g ↑ofNatHom → f = g
ext_int
{f g :
ℤ: Type
ℤ
→*
M: Type ?u.48766
M
} (
h_neg_one: ↑f (-1) = ↑g (-1)
h_neg_one
: f (-
1: ?m.49492
1
) = g (-
1: ?m.49972
1
)) (
h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom
h_nat
: f.
comp: {M : Type ?u.49996} → {N : Type ?u.49995} → {P : Type ?u.49994} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (N →* P) → (M →* N) → M →* P
comp
Int.ofNatHom: ℕ →+* ℤ
Int.ofNatHom
.
toMonoidHom: {α : Type ?u.50012} → {β : Type ?u.50011} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →* β
toMonoidHom
= g.
comp: {M : Type ?u.50069} → {N : Type ?u.50068} → {P : Type ?u.50067} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (N →* P) → (M →* N) → M →* P
comp
Int.ofNatHom: ℕ →+* ℤ
Int.ofNatHom
.
toMonoidHom: {α : Type ?u.50085} → {β : Type ?u.50084} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →* β
toMonoidHom
) : f = g :=

Goals accomplished! 🐙
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom


f = g
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.ofNat
↑f (ofNat x) = ↑g (ofNat x)
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f -[x+1] = ↑g -[x+1]
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom


f = g
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.ofNat
↑f (ofNat x) = ↑g (ofNat x)
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.ofNat
↑f (ofNat x) = ↑g (ofNat x)
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f -[x+1] = ↑g -[x+1]

Goals accomplished! 🐙
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom


f = g
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f -[x+1] = ↑g -[x+1]
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f -[x+1] = ↑g -[x+1]
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f -[x+1] = ↑g -[x+1]
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f (-(↑x + 1)) = ↑g (-(↑x + 1))
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f -[x+1] = ↑g -[x+1]
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f (-1 * (↑x + 1)) = ↑g (-1 * (↑x + 1))
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f -[x+1] = ↑g -[x+1]
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f (-1) * ↑f (↑x + 1) = ↑g (-1 * (↑x + 1))
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f -[x+1] = ↑g -[x+1]
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f (-1) * ↑f (↑x + 1) = ↑g (-1) * ↑g (↑x + 1)
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f (-1) * ↑f (↑x + 1) = ↑g (-1) * ↑g (↑x + 1)
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f -[x+1] = ↑g -[x+1]
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc.e_a
↑f (↑x + 1) = ↑g (↑x + 1)
F: Type ?u.48754

ι: Type ?u.48757

α: Type ?u.48760

β: Type ?u.48763

M: Type u_1

inst✝: Monoid M

f, g: ℤ →* M

h_neg_one: ↑f (-1) = ↑g (-1)

h_nat: comp f ↑ofNatHom = comp g ↑ofNatHom

x: ℕ


h.negSucc
↑f -[x+1] = ↑g -[x+1]

Goals accomplished! 🐙
#align monoid_hom.ext_int
MonoidHom.ext_int: ∀ {M : Type u_1} [inst : Monoid M] {f g : ℤ →* M}, ↑f (-1) = ↑g (-1) → comp f ↑ofNatHom = comp g ↑ofNatHom → f = g
MonoidHom.ext_int
end MonoidHom namespace MonoidWithZeroHom variable {
M: Type ?u.51935
M
:
Type _: Type (?u.51917+1)
Type _
} [
MonoidWithZero: Type ?u.51938 → Type ?u.51938
MonoidWithZero
M: Type ?u.51917
M
] /-- If two `MonoidWithZeroHom`s agree on `-1` and the naturals then they are equal. -/ @[ext] theorem
ext_int: ∀ {M : Type u_1} [inst : MonoidWithZero M] {f g : ℤ →*₀ M}, ↑f (-1) = ↑g (-1) → comp f (RingHom.toMonoidWithZeroHom ofNatHom) = comp g (RingHom.toMonoidWithZeroHom ofNatHom) → f = g
ext_int
{f g :
ℤ: Type
ℤ
→*₀
M: Type ?u.51935
M
} (
h_neg_one: ↑f (-1) = ↑g (-1)
h_neg_one
: f (-
1: ?m.52684
1
) = g (-
1: ?m.53246
1
)) (h_nat : f.
comp: {M : Type ?u.53270} → {N : Type ?u.53269} → {P : Type ?u.53268} → [inst : MulZeroOneClass M] → [inst_1 : MulZeroOneClass N] → [inst_2 : MulZeroOneClass P] → (N →*₀ P) → (M →*₀ N) → M →*₀ P
comp
Int.ofNatHom: ℕ →+* ℤ
Int.ofNatHom
.
toMonoidWithZeroHom: {α : Type ?u.53286} → {β : Type ?u.53285} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →*₀ β
toMonoidWithZeroHom
= g.
comp: {M : Type ?u.53344} → {N : Type ?u.53343} → {P : Type ?u.53342} → [inst : MulZeroOneClass M] → [inst_1 : MulZeroOneClass N] → [inst_2 : MulZeroOneClass P] → (N →*₀ P) → (M →*₀ N) → M →*₀ P
comp
Int.ofNatHom: ℕ →+* ℤ
Int.ofNatHom
.
toMonoidWithZeroHom: {α : Type ?u.53360} → {β : Type ?u.53359} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →*₀ β
toMonoidWithZeroHom
) : f = g :=
toMonoidHom_injective: ∀ {M : Type ?u.53384} {N : Type ?u.53385} [inst : MulZeroOneClass M] [inst_1 : MulZeroOneClass N], Function.Injective toMonoidHom
toMonoidHom_injective
<|
MonoidHom.ext_int: ∀ {M : Type ?u.53418} [inst : Monoid M] {f g : ℤ →* M}, ↑f (-1) = ↑g (-1) → MonoidHom.comp f ↑ofNatHom = MonoidHom.comp g ↑ofNatHom → f = g
MonoidHom.ext_int
h_neg_one: ↑f (-1) = ↑g (-1)
h_neg_one
<|
MonoidHom.ext: ∀ {M : Type ?u.53473} {N : Type ?u.53474} [inst : MulOneClass M] [inst_1 : MulOneClass N] ⦃f g : M →* N⦄, (∀ (x : M), ↑f x = ↑g x) → f = g
MonoidHom.ext
(
FunLike.congr_fun: ∀ {F : Sort ?u.53514} {α : Sort ?u.53516} {β : α → Sort ?u.53515} [i : FunLike F α β] {f g : F}, f = g → ∀ (x : α), ↑f x = ↑g x
FunLike.congr_fun
h_nat :
_: Sort ?u.53512
_
) #align monoid_with_zero_hom.ext_int
MonoidWithZeroHom.ext_int: ∀ {M : Type u_1} [inst : MonoidWithZero M] {f g : ℤ →*₀ M}, ↑f (-1) = ↑g (-1) → comp f (RingHom.toMonoidWithZeroHom ofNatHom) = comp g (RingHom.toMonoidWithZeroHom ofNatHom) → f = g
MonoidWithZeroHom.ext_int
end MonoidWithZeroHom /-- If two `MonoidWithZeroHom`s agree on `-1` and the _positive_ naturals then they are equal. -/ theorem
ext_int': ∀ [inst : MonoidWithZero α] [inst_1 : MonoidWithZeroHomClass F ℤ α] {f g : F}, ↑f (-1) = ↑g (-1) → (∀ (n : ℕ), 0 < n → ↑f ↑n = ↑g ↑n) → f = g
ext_int'
[
MonoidWithZero: Type ?u.54423 → Type ?u.54423
MonoidWithZero
α: Type ?u.54417
α
] [
MonoidWithZeroHomClass: Type ?u.54428 → (M : outParam (Type ?u.54427)) → (N : outParam (Type ?u.54426)) → [inst : MulZeroOneClass M] → [inst : MulZeroOneClass N] → Type (max(max?u.54428?u.54427)?u.54426)
MonoidWithZeroHomClass
F: Type ?u.54411
F
ℤ: Type
ℤ
α: Type ?u.54417
α
] {
f: F
f
g: F
g
:
F: Type ?u.54411
F
} (
h_neg_one: ↑f (-1) = ↑g (-1)
h_neg_one
:
f: F
f
(-
1: ?m.55159
1
) =
g: F
g
(-
1: ?m.55715
1
)) (
h_pos: ∀ (n : ℕ), 0 < n → ↑f ↑n = ↑g ↑n
h_pos
: ∀ n :
ℕ: Type
ℕ
,
0: ?m.55742
0
< n →
f: F
f
n =
g: F
g
n) :
f: F
f
=
g: F
g
:= (
FunLike.ext: ∀ {F : Sort ?u.56869} {α : Sort ?u.56870} {β : α → Sort ?u.56868} [i : FunLike F α β] (f g : F), (∀ (x : α), ↑f x = ↑g x) → f = g
FunLike.ext
_: ?m.56871
_
_: ?m.56871
_
) fun
n: ?m.56912
n
=> haveI :=
FunLike.congr_fun: ∀ {F : Sort ?u.56916} {α : Sort ?u.56918} {β : α → Sort ?u.56917} [i : FunLike F α β] {f g : F}, f = g → ∀ (x : α), ↑f x = ↑g x
FunLike.congr_fun
(@
MonoidWithZeroHom.ext_int: ∀ {M : Type ?u.56925} [inst : MonoidWithZero M] {f g : ℤ →*₀ M}, ↑f (-1) = ↑g (-1) → MonoidWithZeroHom.comp f (RingHom.toMonoidWithZeroHom ofNatHom) = MonoidWithZeroHom.comp g (RingHom.toMonoidWithZeroHom ofNatHom) → f = g
MonoidWithZeroHom.ext_int
_: Type ?u.56925
_
_ (
f: F
f
:
ℤ: Type
ℤ
→*₀
α: Type ?u.54417
α
) (
g: F
g
:
ℤ: Type
ℤ
→*₀
α: Type ?u.54417
α
)
h_neg_one: ↑f (-1) = ↑g (-1)
h_neg_one
<|
MonoidWithZeroHom.ext_nat: ∀ {A : Type ?u.57299} [inst : MulZeroOneClass A] {f g : ℕ →*₀ A}, (∀ {n : ℕ}, 0 < n → ↑f n = ↑g n) → f = g
MonoidWithZeroHom.ext_nat
(
h_pos: ∀ (n : ℕ), 0