/-
Copyright (c) 2014 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 algebra.char_zero.lemmas
! leanprover-community/mathlib commit acee671f47b8e7972a1eb6f4eed74b4b3abce829
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Cast.Field
import Mathlib.Algebra.GroupPower.Lemmas

/-!
# Characteristic zero (additional theorems)

A ring `R` is called of characteristic zero if every natural number `n` is non-zero when considered
as an element of `R`. Since this definition doesn't mention the multiplicative structure of `R`
except for the existence of `1` in this file characteristic zero is defined for additive monoids
with `1`.

## Main statements

* Characteristic zero implies that the additive monoid is infinite.
-/


namespace Nat

variable {R: Type ?u.2
R : Type _: Type (?u.2+1)
Type _} [AddMonoidWithOne: Type ?u.5 → Type ?u.5
AddMonoidWithOne R: Type ?u.2
R] [CharZero: (R : Type ?u.23) → [inst : AddMonoidWithOne R] → Prop
CharZero R: Type ?u.2
R]

/-- `Nat.cast` as an embedding into monoids of characteristic `0`. -/
@[simps: ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] (a : ℕ), ↑castEmbedding a = ↑a
simps]
def castEmbedding: {R : Type u_1} → [inst : AddMonoidWithOne R] → [inst : CharZero R] → ℕ ↪ R
castEmbedding : ℕ: Type
ℕ ↪ R: Type ?u.17
R :=
  ⟨Nat.cast: {R : Type ?u.45} → [inst : NatCast R] → ℕ → R
Nat.cast, cast_injective: ∀ {R : Type ?u.300} [inst : AddMonoidWithOne R] [inst_1 : CharZero R], Function.Injective Nat.cast
cast_injective⟩
#align nat.cast_embedding Nat.castEmbedding: {R : Type u_1} → [inst : AddMonoidWithOne R] → [inst : CharZero R] → ℕ ↪ R
Nat.castEmbedding
#align nat.cast_embedding_apply Nat.castEmbedding_apply: ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] (a : ℕ), ↑castEmbedding a = ↑a
Nat.castEmbedding_apply

@[simp]
theorem cast_pow_eq_one: ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : CharZero R] (q n : ℕ), n ≠ 0 → (↑q ^ n = 1 ↔ q = 1)
cast_pow_eq_one {R: Type u_1
R : Type _: Type (?u.415+1)
Type _} [Semiring: Type ?u.418 → Type ?u.418
Semiring R: Type ?u.415
R] [CharZero: (R : Type ?u.421) → [inst : AddMonoidWithOne R] → Prop
CharZero R: Type ?u.415
R] (q: ℕ
q : ℕ: Type
ℕ) (n: ℕ
n : ℕ: Type
ℕ) (hn: n ≠ 0
hn : n: ℕ
n ≠ 0: ?m.554
0) :
    (q: ℕ
q : R: Type ?u.415
R) ^ n: ℕ
n = 1: ?m.622
1 ↔ q: ℕ
q = 1: ?m.781
1 := by
Goals accomplished! 🐙
  R✝: Type ?u.400

inst✝³: AddMonoidWithOne R✝

inst✝²: CharZero R✝

R: Type u_1

inst✝¹: Semiring R

inst✝: CharZero R

q, n: ℕ

hn: n ≠ 0

↑q ^ n = 1 ↔ q = 1rw [R✝: Type ?u.400

inst✝³: AddMonoidWithOne R✝

inst✝²: CharZero R✝

R: Type u_1

inst✝¹: Semiring R

inst✝: CharZero R

q, n: ℕ

hn: n ≠ 0

↑q ^ n = 1 ↔ q = 1← cast_pow: ∀ {R : Type ?u.810} [inst : Semiring R] (n m : ℕ), ↑(n ^ m) = ↑n ^ m
cast_pow,R✝: Type ?u.400

inst✝³: AddMonoidWithOne R✝

inst✝²: CharZero R✝

R: Type u_1

inst✝¹: Semiring R

inst✝: CharZero R

q, n: ℕ

hn: n ≠ 0

↑(q ^ n) = 1 ↔ q = 1 R✝: Type ?u.400

inst✝³: AddMonoidWithOne R✝

inst✝²: CharZero R✝

R: Type u_1

inst✝¹: Semiring R

inst✝: CharZero R

q, n: ℕ

hn: n ≠ 0

↑q ^ n = 1 ↔ q = 1cast_eq_one: ∀ {R : Type ?u.856} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {n : ℕ}, ↑n = 1 ↔ n = 1
cast_eq_oneR✝: Type ?u.400

inst✝³: AddMonoidWithOne R✝

inst✝²: CharZero R✝

R: Type u_1

inst✝¹: Semiring R

inst✝: CharZero R

q, n: ℕ

hn: n ≠ 0

q ^ n = 1 ↔ q = 1]R✝: Type ?u.400

inst✝³: AddMonoidWithOne R✝

inst✝²: CharZero R✝

R: Type u_1

inst✝¹: Semiring R

inst✝: CharZero R

q, n: ℕ

hn: n ≠ 0

q ^ n = 1 ↔ q = 1
  R✝: Type ?u.400

inst✝³: AddMonoidWithOne R✝

inst✝²: CharZero R✝

R: Type u_1

inst✝¹: Semiring R

inst✝: CharZero R

q, n: ℕ

hn: n ≠ 0

↑q ^ n = 1 ↔ q = 1exact pow_eq_one_iff: ∀ {M : Type ?u.1035} [inst : Monoid M] [inst_1 : LinearOrder M]
  [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {x : M} {n : ℕ}, n ≠ 0 → (x ^ n = 1 ↔ x = 1)
pow_eq_one_iff hn: n ≠ 0
hn
Goals accomplished! 🐙
#align nat.cast_pow_eq_one Nat.cast_pow_eq_one: ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : CharZero R] (q n : ℕ), n ≠ 0 → (↑q ^ n = 1 ↔ q = 1)
Nat.cast_pow_eq_one

@[simp, norm_cast]
theorem cast_div_charZero: ∀ {k : Type u_1} [inst : DivisionSemiring k] [inst_1 : CharZero k] {m n : ℕ}, n ∣ m → ↑(m / n) = ↑m / ↑n
cast_div_charZero {k: Type ?u.1363
k : Type _: Type (?u.1363+1)
Type _} [DivisionSemiring: Type ?u.1366 → Type ?u.1366
DivisionSemiring k: Type ?u.1363
k] [CharZero: (R : Type ?u.1369) → [inst : AddMonoidWithOne R] → Prop
CharZero k: Type ?u.1363
k] {m: ℕ
m n: ℕ
n : ℕ: Type
ℕ} (n_dvd: n ∣ m
n_dvd : n: ℕ
n ∣ m: ℕ
m) :
    ((m: ℕ
m / n: ℕ
n : ℕ: Type
ℕ) : k: Type ?u.1363
k) = m: ℕ
m / n: ℕ
n := by
Goals accomplished! 🐙
  R: Type ?u.1348

inst✝³: AddMonoidWithOne R

inst✝²: CharZero R

k: Type u_1

inst✝¹: DivisionSemiring k

inst✝: CharZero k

m, n: ℕ

n_dvd: n ∣ m

↑(m / n) = ↑m / ↑nrcases eq_or_ne: ∀ {α : Sort ?u.2383} (x y : α), x = y ∨ x ≠ y
eq_or_ne n: ℕ
n 0: ?m.2386
0 with (rfl | hn): n = 0 ∨ n ≠ 0
(rfl: n = 0
rflrfl | hn: n = 0 ∨ n ≠ 0
 | hn: n ≠ 0
hn(rfl | hn): n = 0 ∨ n ≠ 0
)R: Type ?u.1348

inst✝³: AddMonoidWithOne R

inst✝²: CharZero R

k: Type u_1

inst✝¹: DivisionSemiring k

inst✝: CharZero k

m: ℕ

n_dvd: 0 ∣ m

inl↑(m / 0) = ↑m / ↑0
R: Type ?u.1348

inst✝³: AddMonoidWithOne R

inst✝²: CharZero R

k: Type u_1

inst✝¹: DivisionSemiring k

inst✝: CharZero k

m, n: ℕ

n_dvd: n ∣ m

hn: n ≠ 0

inr↑(m / n) = ↑m / ↑n
  R: Type ?u.1348

inst✝³: AddMonoidWithOne R

inst✝²: CharZero R

k: Type u_1

inst✝¹: DivisionSemiring k

inst✝: CharZero k

m, n: ℕ

n_dvd: n ∣ m

↑(m / n) = ↑m / ↑n·R: Type ?u.1348

inst✝³: AddMonoidWithOne R

inst✝²: CharZero R

k: Type u_1

inst✝¹: DivisionSemiring k

inst✝: CharZero k

m: ℕ

n_dvd: 0 ∣ m

inl↑(m / 0) = ↑m / ↑0 R: Type ?u.1348

inst✝³: AddMonoidWithOne R

inst✝²: CharZero R

k: Type u_1

inst✝¹: DivisionSemiring k

inst✝: CharZero k

m: ℕ

n_dvd: 0 ∣ m

inl↑(m / 0) = ↑m / ↑0
R: Type ?u.1348

inst✝³: AddMonoidWithOne R

inst✝²: CharZero R

k: Type u_1

inst✝¹: DivisionSemiring k

inst✝: CharZero k

m, n: ℕ

n_dvd: n ∣ m

hn: n ≠ 0

inr↑(m / n) = ↑m / ↑nsimp
Goals accomplished! 🐙
  R: Type ?u.1348

inst✝³: AddMonoidWithOne R

inst✝²: CharZero R

k: Type u_1

inst✝¹: DivisionSemiring k

inst✝: CharZero k

m, n: ℕ

n_dvd: n ∣ m

↑(m / n) = ↑m / ↑n·R: Type ?u.1348

inst✝³: AddMonoidWithOne R

inst✝²: CharZero R

k: Type u_1

inst✝¹: DivisionSemiring k

inst✝: CharZero k

m, n: ℕ

n_dvd: n ∣ m

hn: n ≠ 0

inr↑(m / n) = ↑m / ↑n R: Type ?u.1348

inst✝³: AddMonoidWithOne R

inst✝²: CharZero R

k: Type u_1

inst✝¹: DivisionSemiring k

inst✝: CharZero k

m, n: ℕ

n_dvd: n ∣ m

hn: n ≠ 0

inr↑(m / n) = ↑m / ↑nexact cast_div: ∀ {α : Type ?u.3093} [inst : DivisionSemiring α] {m n : ℕ}, n ∣ m → ↑n ≠ 0 → ↑(m / n) = ↑m / ↑n
cast_div n_dvd: n ∣ m
n_dvd (cast_ne_zero: ∀ {R : Type ?u.3119} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {n : ℕ}, ↑n ≠ 0 ↔ n ≠ 0
cast_ne_zero.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hn: n ≠ 0
hn)
Goals accomplished! 🐙
#align nat.cast_div_char_zero Nat.cast_div_charZero: ∀ {k : Type u_1} [inst : DivisionSemiring k] [inst_1 : CharZero k] {m n : ℕ}, n ∣ m → ↑(m / n) = ↑m / ↑n
Nat.cast_div_charZero

end Nat

section

variable (M: Type ?u.3310
M : Type _: Type (?u.3310+1)
Type _) [AddMonoidWithOne: Type ?u.3298 → Type ?u.3298
AddMonoidWithOne M: Type ?u.3295
M] [CharZero: (R : Type ?u.3301) → [inst : AddMonoidWithOne R] → Prop
CharZero M: Type ?u.3295
M]

instance CharZero.NeZero.two: NeZero 2
CharZero.NeZero.two : NeZero: {R : Type ?u.3325} → [inst : Zero R] → R → Prop
NeZero (2: ?m.3364
2 : M: Type ?u.3310
M) :=
  ⟨by
Goals accomplished! 🐙
    M: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M

2 ≠ 0have : ((2: ?m.4131
2 : ℕ: Type
ℕ) : M: Type ?u.3310
M) ≠ 0: ?m.4352
0 := Nat.cast_ne_zero: ∀ {R : Type ?u.4758} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {n : ℕ}, ↑n ≠ 0 ↔ n ≠ 0
Nat.cast_ne_zero.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (M: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M

2 ≠ 0by
Goals accomplished! 🐙 M: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M

2 ≠ 0decide
Goals accomplished! 🐙)M: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M

this: ↑2 ≠ 0

2 ≠ 0
    M: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M

2 ≠ 0rwa [M: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M

this: ↑2 ≠ 0

2 ≠ 0Nat.cast_two: ∀ {R : Type ?u.4830} [inst : AddMonoidWithOne R], ↑2 = 2
Nat.cast_twoM: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M

this: 2 ≠ 0

2 ≠ 0]M: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M

this: 2 ≠ 0

2 ≠ 0 at this: ↑2 ≠ 0
this
Goals accomplished! 🐙⟩
#align char_zero.ne_zero.two CharZero.NeZero.two: ∀ (M : Type u_1) [inst : AddMonoidWithOne M] [inst_1 : CharZero M], NeZero 2
CharZero.NeZero.two

end

section

variable {R: Type ?u.8459
R : Type _: Type (?u.8459+1)
Type _} [NonAssocSemiring: Type ?u.7436 → Type ?u.7436
NonAssocSemiring R: Type ?u.4919
R] [NoZeroDivisors: (M₀ : Type ?u.4925) → [inst : Mul M₀] → [inst : Zero M₀] → Prop
NoZeroDivisors R: Type ?u.8459
R] [CharZero: (R : Type ?u.8856) → [inst : AddMonoidWithOne R] → Prop
CharZero R: Type ?u.5409
R] {a: R
a : R: Type ?u.4919
R}

@[simp]
theorem add_self_eq_zero: ∀ {a : R}, a + a = 0 ↔ a = 0
add_self_eq_zero {a: R
a : R: Type ?u.5409
R} : a: R
a + a: R
a = 0: ?m.5906
0 ↔ a: R
a = 0: ?m.6429
0 := by
Goals accomplished! 🐙
  R: Type u_1

inst✝²: NonAssocSemiring R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a✝, a: R

a + a = 0 ↔ a = 0simp only [(two_mul: ∀ {α : Type ?u.6461} [inst : NonAssocSemiring α] (n : α), 2 * n = n + n
two_mul a: R
a).symm: ∀ {α : Sort ?u.6468} {a b : α}, a = b → b = a
symm, mul_eq_zero: ∀ {M₀ : Type ?u.6485} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, a * b = 0 ↔ a = 0 ∨ b = 0
mul_eq_zero, two_ne_zero: ∀ {α : Type ?u.6516} [inst : Zero α] [inst_1 : OfNat α 2] [inst_2 : NeZero 2], 2 ≠ 0
two_ne_zero, false_or_iff: ∀ (p : Prop), False ∨ p ↔ p
false_or_iff]
Goals accomplished! 🐙
#align add_self_eq_zero add_self_eq_zero: ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  a + a = 0 ↔ a = 0
add_self_eq_zero

set_option linter.deprecated false

@[simp]
theorem bit0_eq_zero: ∀ {a : R}, bit0 a = 0 ↔ a = 0
bit0_eq_zero {a: R
a : R: Type ?u.7433
R} : bit0: {α : Type ?u.7926} → [inst : Add α] → α → α
bit0 a: R
a = 0: ?m.8054
0 ↔ a: R
a = 0: ?m.8339
0 :=
  add_self_eq_zero: ∀ {R : Type ?u.8357} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  a + a = 0 ↔ a = 0
add_self_eq_zero
#align bit0_eq_zero bit0_eq_zero: ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  bit0 a = 0 ↔ a = 0
bit0_eq_zero

@[simp]
theorem zero_eq_bit0: ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  0 = bit0 a ↔ a = 0
zero_eq_bit0 {a: R
a : R: Type ?u.8459
R} : 0: ?m.8953
0 = bit0: {α : Type ?u.8968} → [inst : Add α] → α → α
bit0 a: R
a ↔ a: R
a = 0: ?m.9370
0 := by
Goals accomplished! 🐙
  R: Type u_1

inst✝²: NonAssocSemiring R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a✝, a: R

0 = bit0 a ↔ a = 0rw [R: Type u_1

inst✝²: NonAssocSemiring R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a✝, a: R

0 = bit0 a ↔ a = 0eq_comm: ∀ {α : Sort ?u.9390} {a b : α}, a = b ↔ b = a
eq_commR: Type u_1

inst✝²: NonAssocSemiring R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a✝, a: R

bit0 a = 0 ↔ a = 0]R: Type u_1

inst✝²: NonAssocSemiring R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a✝, a: R

bit0 a = 0 ↔ a = 0
  R: Type u_1

inst✝²: NonAssocSemiring R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a✝, a: R

0 = bit0 a ↔ a = 0exact bit0_eq_zero: ∀ {R : Type ?u.9411} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  bit0 a = 0 ↔ a = 0
bit0_eq_zero
Goals accomplished! 🐙
#align zero_eq_bit0 zero_eq_bit0: ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  0 = bit0 a ↔ a = 0
zero_eq_bit0

theorem bit0_ne_zero: ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  bit0 a ≠ 0 ↔ a ≠ 0
bit0_ne_zero : bit0: {α : Type ?u.9994} → [inst : Add α] → α → α
bit0 a: R
a ≠ 0: ?m.10143
0 ↔ a: R
a ≠ 0: ?m.10415
0 :=
  bit0_eq_zero: ∀ {R : Type ?u.10418} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  bit0 a = 0 ↔ a = 0
bit0_eq_zero.not: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not
#align bit0_ne_zero bit0_ne_zero: ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  bit0 a ≠ 0 ↔ a ≠ 0
bit0_ne_zero

theorem zero_ne_bit0: 0 ≠ bit0 a ↔ a ≠ 0
zero_ne_bit0 : 0: ?m.10986
0 ≠ bit0: {α : Type ?u.10996} → [inst : Add α] → α → α
bit0 a: R
a ↔ a: R
a ≠ 0: ?m.11147
0 :=
  zero_eq_bit0: ∀ {R : Type ?u.11417} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  0 = bit0 a ↔ a = 0
zero_eq_bit0.not: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not
#align zero_ne_bit0 zero_ne_bit0: ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  0 ≠ bit0 a ↔ a ≠ 0
zero_ne_bit0

end

section

variable {R: Type ?u.14297
R : Type _: Type (?u.11497+1)
Type _} [NonAssocRing: Type ?u.14300 → Type ?u.14300
NonAssocRing R: Type ?u.18277
R] [NoZeroDivisors: (M₀ : Type ?u.16745) → [inst : Mul M₀] → [inst : Zero M₀] → Prop
NoZeroDivisors R: Type ?u.11497
R] [CharZero: (R : Type ?u.16103) → [inst : AddMonoidWithOne R] → Prop
CharZero R: Type ?u.11497
R]

theorem neg_eq_self_iff: ∀ {a : R}, -a = a ↔ a = 0
neg_eq_self_iff {a: R
a : R: Type ?u.11895
R} : -a: R
a = a: R
a ↔ a: R
a = 0: ?m.12406
0 :=
  neg_eq_iff_add_eq_zero: ∀ {G : Type ?u.12698} [inst : AddGroup G] {a b : G}, -a = b ↔ a + b = 0
neg_eq_iff_add_eq_zero.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans add_self_eq_zero: ∀ {R : Type ?u.12742} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  a + a = 0 ↔ a = 0
add_self_eq_zero
#align neg_eq_self_iff neg_eq_self_iff: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R}, -a = a ↔ a = 0
neg_eq_self_iff

theorem eq_neg_self_iff: ∀ {a : R}, a = -a ↔ a = 0
eq_neg_self_iff {a: R
a : R: Type ?u.13096
R} : a: R
a = -a: R
a ↔ a: R
a = 0: ?m.13607
0 :=
  eq_neg_iff_add_eq_zero: ∀ {G : Type ?u.13899} [inst : AddGroup G] {a b : G}, a = -b ↔ a + b = 0
eq_neg_iff_add_eq_zero.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans add_self_eq_zero: ∀ {R : Type ?u.13943} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  a + a = 0 ↔ a = 0
add_self_eq_zero
#align eq_neg_self_iff eq_neg_self_iff: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R}, a = -a ↔ a = 0
eq_neg_self_iff

theorem nat_mul_inj: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {n : ℕ} {a b : R},
  ↑n * a = ↑n * b → n = 0 ∨ a = b
nat_mul_inj {n: ℕ
n : ℕ: Type
ℕ} {a: R
a b: R
b : R: Type ?u.14297
R} (h: ↑n * a = ↑n * b
h : (n: ℕ
n : R: Type ?u.14297
R) * a: R
a = (n: ℕ
n : R: Type ?u.14297
R) * b: R
b) : n: ℕ
n = 0: ?m.15050
0 ∨ a: R
a = b: R
b := by
Goals accomplished! 🐙
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h: ↑n * a = ↑n * b

n = 0 ∨ a = brw [R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h: ↑n * a = ↑n * b

n = 0 ∨ a = b← sub_eq_zero: ∀ {G : Type ?u.15083} [inst : AddGroup G] {a b : G}, a - b = 0 ↔ a = b
sub_eq_zero,R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h✝: ↑n * a = ↑n * b

h: ↑n * a - ↑n * b = 0

n = 0 ∨ a = b R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h: ↑n * a = ↑n * b

n = 0 ∨ a = b← mul_sub: ∀ {α : Type ?u.15221} [inst : NonUnitalNonAssocRing α] (a b c : α), a * (b - c) = a * b - a * c
mul_sub,R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h✝: ↑n * a = ↑n * b

h: ↑n * (a - b) = 0

n = 0 ∨ a = b R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h: ↑n * a = ↑n * b

n = 0 ∨ a = bmul_eq_zero: ∀ {M₀ : Type ?u.15283} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, a * b = 0 ↔ a = 0 ∨ b = 0
mul_eq_zero,R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h✝: ↑n * a = ↑n * b

h: ↑n = 0 ∨ a - b = 0

n = 0 ∨ a = b R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h: ↑n * a = ↑n * b

n = 0 ∨ a = bsub_eq_zero: ∀ {G : Type ?u.15379} [inst : AddGroup G] {a b : G}, a - b = 0 ↔ a = b
sub_eq_zeroR: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h✝: ↑n * a = ↑n * b

h: ↑n = 0 ∨ a = b

n = 0 ∨ a = b]R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h✝: ↑n * a = ↑n * b

h: ↑n = 0 ∨ a = b

n = 0 ∨ a = b at h: ↑n = 0 ∨ a - b = 0
hR: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h✝: ↑n * a = ↑n * b

h: ↑n = 0 ∨ a = b

n = 0 ∨ a = b
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h: ↑n * a = ↑n * b

n = 0 ∨ a = bexact_mod_cast h: ↑n = 0 ∨ a = b
h
Goals accomplished! 🐙
#align nat_mul_inj nat_mul_inj: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {n : ℕ} {a b : R},
  ↑n * a = ↑n * b → n = 0 ∨ a = b
nat_mul_inj

theorem nat_mul_inj': ∀ {n : ℕ} {a b : R}, ↑n * a = ↑n * b → n ≠ 0 → a = b
nat_mul_inj' {n: ℕ
n : ℕ: Type
ℕ} {a: R
a b: R
b : R: Type ?u.15782
R} (h: ↑n * a = ↑n * b
h : (n: ℕ
n : R: Type ?u.15782
R) * a: R
a = (n: ℕ
n : R: Type ?u.15782
R) * b: R
b) (w: n ≠ 0
w : n: ℕ
n ≠ 0: ?m.16536
0) : a: R
a = b: R
b := by
Goals accomplished! 🐙
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

n: ℕ

a, b: R

h: ↑n * a = ↑n * b

w: n ≠ 0

a = bsimpa [w: n ≠ 0
w] using nat_mul_inj: ∀ {R : Type ?u.16599} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {n : ℕ} {a b : R},
  ↑n * a = ↑n * b → n = 0 ∨ a = b
nat_mul_inj h: ↑n * a = ↑n * b
h
Goals accomplished! 🐙
#align nat_mul_inj' nat_mul_inj': ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {n : ℕ} {a b : R},
  ↑n * a = ↑n * b → n ≠ 0 → a = b
nat_mul_inj'

set_option linter.deprecated false

theorem bit0_injective: Function.Injective bit0
bit0_injective : Function.Injective: {α : Sort ?u.17138} → {β : Sort ?u.17137} → (α → β) → Prop
Function.Injective (bit0: {α : Type ?u.17144} → [inst : Add α] → α → α
bit0 : R: Type ?u.16739
R → R: Type ?u.16739
R) := fun a: ?m.17204
a b: ?m.17207
b h: ?m.17210
h => by
Goals accomplished! 🐙
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: bit0 a = bit0 b

a = bdsimp [bit0: {α : Type ?u.17217} → [inst : Add α] → α → α
bit0] at h: bit0 a = bit0 b
hR: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: a + a = b + b

a = b
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: bit0 a = bit0 b

a = bsimp only [(two_mul: ∀ {α : Type ?u.17238} [inst : NonAssocSemiring α] (n : α), 2 * n = n + n
two_mul a: R
a).symm: ∀ {α : Sort ?u.17439} {a b : α}, a = b → b = a
symm, (two_mul: ∀ {α : Type ?u.17457} [inst : NonAssocSemiring α] (n : α), 2 * n = n + n
two_mul b: R
b).symm: ∀ {α : Sort ?u.17658} {a b : α}, a = b → b = a
symm] at h: a + a = b + b
hR: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: 2 * a = 2 * b

a = b
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: bit0 a = bit0 b

a = brefine' nat_mul_inj': ∀ {R : Type ?u.17793} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {n : ℕ} {a b : R},
  ↑n * a = ↑n * b → n ≠ 0 → a = b
nat_mul_inj' _: ↑?m.17798 * ?m.17799 = ↑?m.17798 * ?m.17800
_ two_ne_zero: ∀ {α : Type ?u.17821} [inst : Zero α] [inst_1 : OfNat α 2] [inst_2 : NeZero 2], 2 ≠ 0
two_ne_zeroR: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: 2 * a = 2 * b

↑2 * a = ↑2 * b
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: bit0 a = bit0 b

a = bexact_mod_cast h: 2 * a = 2 * b
h
Goals accomplished! 🐙
#align bit0_injective bit0_injective: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R], Function.Injective bit0
bit0_injective

theorem bit1_injective: Function.Injective bit1
bit1_injective : Function.Injective: {α : Sort ?u.18676} → {β : Sort ?u.18675} → (α → β) → Prop
Function.Injective (bit1: {α : Type ?u.18682} → [inst : One α] → [inst : Add α] → α → α
bit1 : R: Type ?u.18277
R → R: Type ?u.18277
R) := fun a: ?m.18984
a b: ?m.18987
b h: ?m.18990
h => by
Goals accomplished! 🐙
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: bit1 a = bit1 b

a = bsimp only [bit1: {α : Type ?u.19008} → [inst : One α] → [inst : Add α] → α → α
bit1, add_left_inj: ∀ {G : Type ?u.19014} [inst : Add G] [inst_1 : IsRightCancelAdd G] (a : G) {b c : G}, b + a = c + a ↔ b = c
add_left_inj] at h: bit1 a = bit1 b
hR: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: bit0 a = bit0 b

a = b
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: bit1 a = bit1 b

a = bexact bit0_injective: ∀ {R : Type ?u.19294} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R], Function.Injective bit0
bit0_injective h: bit0 a = bit0 b
h
Goals accomplished! 🐙
#align bit1_injective bit1_injective: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R], Function.Injective bit1
bit1_injective

@[simp]
theorem bit0_eq_bit0: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a b : R},
  bit0 a = bit0 b ↔ a = b
bit0_eq_bit0 {a: R
a b: R
b : R: Type ?u.19354
R} : bit0: {α : Type ?u.19757} → [inst : Add α] → α → α
bit0 a: R
a = bit0: {α : Type ?u.19790} → [inst : Add α] → α → α
bit0 b: R
b ↔ a: R
a = b: R
b :=
  bit0_injective: ∀ {R : Type ?u.19799} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R], Function.Injective bit0
bit0_injective.eq_iff: ∀ {α : Sort ?u.19823} {β : Sort ?u.19824} {f : α → β}, Function.Injective f → ∀ {a b : α}, f a = f b ↔ a = b
eq_iff
#align bit0_eq_bit0 bit0_eq_bit0: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a b : R},
  bit0 a = bit0 b ↔ a = b
bit0_eq_bit0

@[simp]
theorem bit1_eq_bit1: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a b : R},
  bit1 a = bit1 b ↔ a = b
bit1_eq_bit1 {a: R
a b: R
b : R: Type ?u.19924
R} : bit1: {α : Type ?u.20327} → [inst : One α] → [inst : Add α] → α → α
bit1 a: R
a = bit1: {α : Type ?u.20569} → [inst : One α] → [inst : Add α] → α → α
bit1 b: R
b ↔ a: R
a = b: R
b :=
  bit1_injective: ∀ {R : Type ?u.20579} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R], Function.Injective bit1
bit1_injective.eq_iff: ∀ {α : Sort ?u.20603} {β : Sort ?u.20604} {f : α → β}, Function.Injective f → ∀ {a b : α}, f a = f b ↔ a = b
eq_iff
#align bit1_eq_bit1 bit1_eq_bit1: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a b : R},
  bit1 a = bit1 b ↔ a = b
bit1_eq_bit1

@[simp]
theorem bit1_eq_one: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R}, bit1 a = 1 ↔ a = 0
bit1_eq_one {a: R
a : R: Type ?u.20700
R} : bit1: {α : Type ?u.21101} → [inst : One α] → [inst : Add α] → α → α
bit1 a: R
a = 1: ?m.21344
1 ↔ a: R
a = 0: ?m.21534
0 := by
Goals accomplished! 🐙
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R

bit1 a = 1 ↔ a = 0rw [R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R

bit1 a = 1 ↔ a = 0show (1: ?m.21806
1 : R: Type u_1
R) = bit1: {α : Type ?u.22026} → [inst : One α] → [inst : Add α] → α → α
bit1 0: ?m.22031
0 by R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R

bit1 a = 1 ↔ a = 0simp
Goals accomplished! 🐙,R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R

bit1 a = bit1 0 ↔ a = 0 R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R

bit1 a = 1 ↔ a = 0bit1_eq_bit1: ∀ {R : Type ?u.22756} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a b : R},
  bit1 a = bit1 b ↔ a = b
bit1_eq_bit1R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R

a = 0 ↔ a = 0]
Goals accomplished! 🐙
#align bit1_eq_one bit1_eq_one: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R}, bit1 a = 1 ↔ a = 0
bit1_eq_one

@[simp]
theorem one_eq_bit1: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R}, 1 = bit1 a ↔ a = 0
one_eq_bit1 {a: R
a : R: Type ?u.22857
R} : 1: ?m.23259
1 = bit1: {α : Type ?u.23274} → [inst : One α] → [inst : Add α] → α → α
bit1 a: R
a ↔ a: R
a = 0: ?m.23696
0 := by
Goals accomplished! 🐙
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R

1 = bit1 a ↔ a = 0rw [R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R

1 = bit1 a ↔ a = 0eq_comm: ∀ {α : Sort ?u.23964} {a b : α}, a = b ↔ b = a
eq_commR: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R

bit1 a = 1 ↔ a = 0]R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R

bit1 a = 1 ↔ a = 0
  R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R

1 = bit1 a ↔ a = 0exact bit1_eq_one: ∀ {R : Type ?u.23985} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
  bit1 a = 1 ↔ a = 0
bit1_eq_one
Goals accomplished! 🐙
#align one_eq_bit1 one_eq_bit1: ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R}, 1 = bit1 a ↔ a = 0
one_eq_bit1

end

section

variable {R: Type ?u.24072
R : Type _: Type (?u.24072+1)
Type _} [DivisionRing: Type ?u.25453 → Type ?u.25453
DivisionRing R: Type ?u.24072
R] [CharZero: (R : Type ?u.24078) → [inst : AddMonoidWithOne R] → Prop
CharZero R: Type ?u.24072
R]

@[simp]
theorem half_add_self: ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), (a + a) / 2 = a
half_add_self (a: R
a : R: Type ?u.24147
R) : (a: R
a + a: R
a) / 2: ?m.24232
2 = a: R
a := by
Goals accomplished! 🐙 R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

(a + a) / 2 = arw [R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

(a + a) / 2 = a← mul_two: ∀ {α : Type ?u.24669} [inst : NonAssocSemiring α] (n : α), n * 2 = n + n
mul_two,R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a * 2 / 2 = a R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

(a + a) / 2 = amul_div_cancel: ∀ {G₀ : Type ?u.24859} [inst : GroupWithZero G₀] {b : G₀} (a : G₀), b ≠ 0 → a * b / b = a
mul_div_cancel a: R
a two_ne_zero: ∀ {α : Type ?u.24863} [inst : Zero α] [inst_1 : OfNat α 2] [inst_2 : NeZero 2], 2 ≠ 0
two_ne_zeroR: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a = a]
Goals accomplished! 🐙
#align half_add_self half_add_self: ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), (a + a) / 2 = a
half_add_self

@[simp]
theorem add_halves': ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a / 2 + a / 2 = a
add_halves' (a: R
a : R: Type ?u.25450
R) : a: R
a / 2: ?m.25535
2 + a: R
a / 2: ?m.25548
2 = a: R
a := by
Goals accomplished! 🐙 R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a / 2 + a / 2 = arw [R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a / 2 + a / 2 = a← add_div: ∀ {α : Type ?u.26046} [inst : DivisionSemiring α] (a b c : α), (a + b) / c = a / c + b / c
add_div,R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

(a + a) / 2 = a R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a / 2 + a / 2 = ahalf_add_self: ∀ {R : Type ?u.26118} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), (a + a) / 2 = a
half_add_selfR: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a = a]
Goals accomplished! 🐙
#align add_halves' add_halves': ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a / 2 + a / 2 = a
add_halves'

theorem sub_half: ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a - a / 2 = a / 2
sub_half (a: R
a : R: Type ?u.26193
R) : a: R
a - a: R
a / 2: ?m.26278
2 = a: R
a / 2: ?m.26295
2 := by
Goals accomplished! 🐙 R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a - a / 2 = a / 2rw [R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a - a / 2 = a / 2sub_eq_iff_eq_add: ∀ {G : Type ?u.26753} [inst : AddGroup G] {a b c : G}, a - b = c ↔ a = c + b
sub_eq_iff_eq_add,R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a = a / 2 + a / 2 R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a - a / 2 = a / 2add_halves': ∀ {R : Type ?u.26859} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a / 2 + a / 2 = a
add_halves'R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a = a]
Goals accomplished! 🐙
#align sub_half sub_half: ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a - a / 2 = a / 2
sub_half

theorem half_sub: ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a / 2 - a = -(a / 2)
half_sub (a: R
a : R: Type ?u.26933
R) : a: R
a / 2: ?m.27018
2 - a: R
a = -(a: R
a / 2: ?m.27036
2) := by
Goals accomplished! 🐙 R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a / 2 - a = -(a / 2)rw [R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a / 2 - a = -(a / 2)← neg_sub: ∀ {α : Type ?u.27544} [inst : SubtractionMonoid α] (a b : α), -(a - b) = b - a
neg_sub,R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

-(a - a / 2) = -(a / 2) R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

a / 2 - a = -(a / 2)sub_half: ∀ {R : Type ?u.27667} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a - a / 2 = a / 2
sub_halfR: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R

-(a / 2) = -(a / 2)]
Goals accomplished! 🐙
#align half_sub half_sub: ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a / 2 - a = -(a / 2)
half_sub

end

namespace WithTop

instance: ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R], CharZero (WithTop R)
instance {R: Type ?u.27736
R : Type _: Type (?u.27736+1)
Type _} [AddMonoidWithOne: Type ?u.27739 → Type ?u.27739
AddMonoidWithOne R: Type ?u.27736
R] [CharZero: (R : Type ?u.27742) → [inst : AddMonoidWithOne R] → Prop
CharZero R: Type ?u.27736
R] :
    CharZero: (R : Type ?u.27751) → [inst : AddMonoidWithOne R] → Prop
CharZero (WithTop: Type ?u.27752 → Type ?u.27752
WithTop R: Type ?u.27736
R) where
  cast_injective m: ?m.27782
m n: ?m.27785
n h: ?m.27788
h := by
Goals accomplished! 🐙
    R: Type ?u.27736

inst✝¹: AddMonoidWithOne R

inst✝: CharZero R

m, n: ℕ

h: ↑m = ↑n

m = nrwa [R: Type ?u.27736

inst✝¹: AddMonoidWithOne R

inst✝: CharZero R

m, n: ℕ

h: ↑m = ↑n

m = n← coe_nat: ∀ {α : Type ?u.27796} [inst : AddMonoidWithOne α] (n : ℕ), ↑↑n = ↑n
coe_nat,R: Type ?u.27736

inst✝¹: AddMonoidWithOne R

inst✝: CharZero R

m, n: ℕ

h: ↑↑m = ↑n

m = n R: Type ?u.27736

inst✝¹: AddMonoidWithOne R

inst✝: CharZero R

m, n: ℕ

h: ↑m = ↑n

m = n← coe_nat: ∀ {α : Type ?u.27850} [inst : AddMonoidWithOne α] (n : ℕ), ↑↑n = ↑n
coe_nat n: ℕ
n,R: Type ?u.27736

inst✝¹: AddMonoidWithOne R

inst✝: CharZero R

m, n: ℕ

h: ↑↑m = ↑↑n

m = n R: Type ?u.27736

inst✝¹: AddMonoidWithOne R

inst✝: CharZero R

m, n: ℕ

h: ↑m = ↑n

m = ncoe_eq_coe: ∀ {α : Type ?u.27890} {a b : α}, ↑a = ↑b ↔ a = b
coe_eq_coe,R: Type ?u.27736

inst✝¹: AddMonoidWithOne R

inst✝: CharZero R

m, n: ℕ

h: ↑m = ↑n

m = n R: Type ?u.27736

inst✝¹: AddMonoidWithOne R

inst✝: CharZero R

m, n: ℕ

h: ↑m = ↑n

m = nNat.cast_inj: ∀ {R : Type ?u.27912} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {m n : ℕ}, ↑m = ↑n ↔ m = n
Nat.cast_injR: Type ?u.27736

inst✝¹: AddMonoidWithOne R

inst✝: CharZero R

m, n: ℕ

h: m = n

m = n]R: Type ?u.27736

inst✝¹: AddMonoidWithOne R

inst✝: CharZero R

m, n: ℕ

h: m = n

m = n at h: ↑m = ↑n
h
Goals accomplished! 🐙

end WithTop

section RingHom

variable {R: Type ?u.29119
R S: Type ?u.28006
S : Type _: Type (?u.28015+1)
Type _} [NonAssocSemiring: Type ?u.28021 → Type ?u.28021
NonAssocSemiring R: Type ?u.28003
R] [NonAssocSemiring: Type ?u.29128 → Type ?u.29128
NonAssocSemiring S: Type ?u.28018
S]

theorem RingHom.charZero: ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
  (R →+* S) → ∀ [hS : CharZero S], CharZero R
RingHom.charZero (ϕ: R →+* S
ϕ : R: Type ?u.28015
R →+* S: Type ?u.28018
S) [hS: CharZero S
hS : CharZero: (R : Type ?u.28043) → [inst : AddMonoidWithOne R] → Prop
CharZero S: Type ?u.28018
S] : CharZero: (R : Type ?u.28157) → [inst : AddMonoidWithOne R] → Prop
CharZero R: Type ?u.28015
R :=
  ⟨fun a: ?m.28294
a b: ?m.28297
b h: ?m.28300
h => CharZero.cast_injective: ∀ {R : Type ?u.28302} [inst : AddMonoidWithOne R] [self : CharZero R], Function.Injective Nat.cast
CharZero.cast_injective (by
Goals accomplished! 🐙 R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hS: CharZero S

a, b: ℕ

h: ↑a = ↑b

↑a = ↑brw [R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hS: CharZero S

a, b: ℕ

h: ↑a = ↑b

↑a = ↑b← map_natCast: ∀ {R : Type ?u.28522} {S : Type ?u.28523} {F : Type ?u.28521} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : RingHomClass F R S] (f : F) (n : ℕ), ↑f ↑n = ↑n
map_natCast ϕ: R →+* S
ϕ,R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hS: CharZero S

a, b: ℕ

h: ↑a = ↑b

↑ϕ ↑a = ↑b R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hS: CharZero S

a, b: ℕ

h: ↑a = ↑b

↑a = ↑b← map_natCast: ∀ {R : Type ?u.28914} {S : Type ?u.28915} {F : Type ?u.28913} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : RingHomClass F R S] (f : F) (n : ℕ), ↑f ↑n = ↑n
map_natCast ϕ: R →+* S
ϕ,R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hS: CharZero S

a, b: ℕ

h: ↑a = ↑b

↑ϕ ↑a = ↑ϕ ↑b R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hS: CharZero S

a, b: ℕ

h: ↑a = ↑b

↑a = ↑bh: ↑a = ↑b
hR: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hS: CharZero S

a, b: ℕ

h: ↑a = ↑b

↑ϕ ↑b = ↑ϕ ↑b]
Goals accomplished! 🐙)⟩
#align ring_hom.char_zero RingHom.charZero: ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
  (R →+* S) → ∀ [hS : CharZero S], CharZero R
RingHom.charZero

theorem RingHom.charZero_iff: ∀ {ϕ : R →+* S}, Function.Injective ↑ϕ → (CharZero R ↔ CharZero S)
RingHom.charZero_iff {ϕ: R →+* S
ϕ : R: Type ?u.29119
R →+* S: Type ?u.29122
S} (hϕ: Function.Injective ↑ϕ
hϕ : Function.Injective: {α : Sort ?u.29148} → {β : Sort ?u.29147} → (α → β) → Prop
Function.Injective ϕ: R →+* S
ϕ) : CharZero: (R : Type ?u.29430) → [inst : AddMonoidWithOne R] → Prop
CharZero R: Type ?u.29119
R ↔ CharZero: (R : Type ?u.29541) → [inst : AddMonoidWithOne R] → Prop
CharZero S: Type ?u.29122
S :=
  ⟨fun hR: ?m.29664
hR =>
    ⟨by
Goals accomplished! 🐙 R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

Function.Injective Nat.castintro a: ℕ
a b: ℕ
b h: ↑a = ↑b
hR: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

a, b: ℕ

h: ↑a = ↑b

a = b;R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

a, b: ℕ

h: ↑a = ↑b

a = b R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

Function.Injective Nat.castrwa [R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

a, b: ℕ

h: ↑a = ↑b

a = b← @Nat.cast_inj: ∀ {R : Type ?u.29846} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {m n : ℕ}, ↑m = ↑n ↔ m = n
Nat.cast_inj R: Type u_1
R,R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

a, b: ℕ

h: ↑a = ↑b

↑a = ↑b R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

a, b: ℕ

h: ↑a = ↑b

a = b← hϕ: Function.Injective ↑ϕ
hϕ.eq_iff: ∀ {α : Sort ?u.29967} {β : Sort ?u.29968} {f : α → β}, Function.Injective f → ∀ {a b : α}, f a = f b ↔ a = b
eq_iff,R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

a, b: ℕ

h: ↑a = ↑b

↑ϕ ↑a = ↑ϕ ↑b R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

a, b: ℕ

h: ↑a = ↑b

a = bmap_natCast: ∀ {R : Type ?u.29992} {S : Type ?u.29993} {F : Type ?u.29991} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : RingHomClass F R S] (f : F) (n : ℕ), ↑f ↑n = ↑n
map_natCast ϕ: R →+* S
ϕ,R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

a, b: ℕ

h: ↑a = ↑b

↑a = ↑ϕ ↑b R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

a, b: ℕ

h: ↑a = ↑b

a = bmap_natCast: ∀ {R : Type ?u.30079} {S : Type ?u.30080} {F : Type ?u.30078} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : RingHomClass F R S] (f : F) (n : ℕ), ↑f ↑n = ↑n
map_natCast ϕ: R →+* S
ϕR: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

a, b: ℕ

h: ↑a = ↑b

↑a = ↑b]R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

hϕ: Function.Injective ↑ϕ

hR: CharZero R

a, b: ℕ

h: ↑a = ↑b

↑a = ↑b⟩,
    fun hS: ?m.29803
hS => ϕ: R →+* S
ϕ.charZero: ∀ {R : Type ?u.29805} {S : Type ?u.29806} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
  (R →+* S) → ∀ [hS : CharZero S], CharZero R
charZero⟩
#align ring_hom.char_zero_iff RingHom.charZero_iff: ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {ϕ : R →+* S},
  Function.Injective ↑ϕ → (CharZero R ↔ CharZero S)
RingHom.charZero_iff

theorem RingHom.injective_nat: ∀ {R : Type u_1} [inst : NonAssocSemiring R] (f : ℕ →+* R) [inst_1 : CharZero R], Function.Injective ↑f
RingHom.injective_nat (f: ℕ →+* R
f : ℕ: Type
ℕ →+* R: Type ?u.30168
R) [CharZero: (R : Type ?u.30206) → [inst : AddMonoidWithOne R] → Prop
CharZero R: Type ?u.30168
R] : Function.Injective: {α : Sort ?u.30321} → {β : Sort ?u.30320} → (α → β) → Prop
Function.Injective f: ℕ →+* R
f :=
  Subsingleton.elim: ∀ {α : Sort ?u.30594} [h : Subsingleton α] (a b : α), a = b
Subsingleton.elim (Nat.castRingHom: (α : Type ?u.30597) → [inst : NonAssocSemiring α] → ℕ →+* α
Nat.castRingHom _: Type ?u.30597
_) f: ℕ →+* R
f ▸ Nat.cast_injective: ∀ {R : Type ?u.30634} [inst : AddMonoidWithOne R] [inst_1 : CharZero R], Function.Injective Nat.cast
Nat.cast_injective
#align ring_hom.injective_nat RingHom.injective_nat: ∀ {R : Type u_1} [inst : NonAssocSemiring R] (f : ℕ →+* R) [inst_1 : CharZero R], Function.Injective ↑f
RingHom.injective_nat

end RingHom