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) 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
:=

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 = 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 = 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 = 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 = 1

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
:=

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_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 / n

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 / n

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] → RProp
NeZero
(
2: ?m.3364
2
:
M: Type ?u.3310
M
) := ⟨

Goals accomplished! 🐙
M: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M


2 0
M: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M


2 0

Goals accomplished! 🐙
M: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M


2 0

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 0
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

this: 2 0


2 0
M: Type ?u.3310

inst✝¹: AddMonoidWithOne M

inst✝: CharZero M

this: 2 0


2 0

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
:=

Goals accomplished! 🐙
R: Type u_1

inst✝²: NonAssocSemiring R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a✝, a: R


a + a = 0 a = 0

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
:=

Goals accomplished! 🐙
R: Type u_1

inst✝²: NonAssocSemiring R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a✝, a: R


0 = bit0 a a = 0
R: Type u_1

inst✝²: NonAssocSemiring R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a✝, a: R


0 = bit0 a 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


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 = 0

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 * bn = 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
:=

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 = 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
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
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 = 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 = 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
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
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
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
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

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 * bn = 0 a = b
nat_mul_inj
theorem
nat_mul_inj': ∀ {n : } {a b : R}, n * a = n * bn 0a = 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
:=

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 = b

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 * bn 0a = 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
=>

Goals accomplished! 🐙
R: 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: 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 = b
R: 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 = b
R: 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 = b

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
=>

Goals accomplished! 🐙
R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: bit1 a = bit1 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 = b
R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a, b: R

h: bit1 a = bit1 b


a = b

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
:=

Goals accomplished! 🐙
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


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

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 = 0
R: 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
:=

Goals accomplished! 🐙
R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R


1 = bit1 a a = 0
R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R


1 = bit1 a 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


bit1 a = 1 a = 0
R: Type u_1

inst✝²: NonAssocRing R

inst✝¹: NoZeroDivisors R

inst✝: CharZero R

a: R


1 = bit1 a a = 0

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
:=

Goals accomplished! 🐙
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 + a) / 2 = a
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 = a
R: 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
:=

Goals accomplished! 🐙
R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R


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

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R


a / 2 + a / 2 = a
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 = a
R: 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
:=

Goals accomplished! 🐙
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 / 2
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 / 2
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
) :=

Goals accomplished! 🐙
R: Type u_1

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R


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

inst✝¹: DivisionRing R

inst✝: CharZero R

a: R


a / 2 - a = -(a / 2)
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)
R: 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
:=

Goals accomplished! 🐙
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
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
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
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
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

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
(

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 = 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
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
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
R: 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
} ( :
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
=> ⟨

Goals accomplished! 🐙
R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

: Function.Injective ϕ

hR: CharZero R


R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

: 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

: 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

: Function.Injective ϕ

hR: CharZero R


R: Type u_1

S: Type u_2

inst✝¹: NonAssocSemiring R

inst✝: NonAssocSemiring S

ϕ: R →+* S

: 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

: 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

: 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

: 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

: 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

: 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

: 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

: 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

: 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