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.
```/-
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

/-!

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.2R : Type _: Type (?u.2+1)Type _} [AddMonoidWithOne: Type ?u.5 β Type ?u.5AddMonoidWithOne R: Type ?u.2R] [CharZero: (R : Type ?u.23) β [inst : AddMonoidWithOne R] β PropCharZero R: Type ?u.2R]

/-- `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 = βasimps]
def castEmbedding: {R : Type u_1} β [inst : AddMonoidWithOne R] β [inst : CharZero R] β β βͺ RcastEmbedding : β: Typeβ βͺ R: Type ?u.17R :=
β¨Nat.cast: {R : Type ?u.45} β [inst : NatCast R] β β β RNat.cast, cast_injective: β {R : Type ?u.300} [inst : AddMonoidWithOne R] [inst_1 : CharZero R], Function.Injective Nat.castcast_injectiveβ©
#align nat.cast_embedding Nat.castEmbedding: {R : Type u_1} β [inst : AddMonoidWithOne R] β [inst : CharZero R] β β βͺ RNat.castEmbedding
#align nat.cast_embedding_apply Nat.castEmbedding_apply: β {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] (a : β), βcastEmbedding a = βaNat.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_1R : Type _: Type (?u.415+1)Type _} [Semiring: Type ?u.418 β Type ?u.418Semiring R: Type ?u.415R] [CharZero: (R : Type ?u.421) β [inst : AddMonoidWithOne R] β PropCharZero R: Type ?u.415R] (q: βq : β: Typeβ) (n: βn : β: Typeβ) (hn: n β  0hn : n: βn β  0: ?m.5540) :
(q: βq : R: Type ?u.415R) ^ n: βn = 1: ?m.6221 β q: βq = 1: ?m.7811 := byGoals accomplished! π
Rβ: Type ?u.400instβΒ³: AddMonoidWithOne RβinstβΒ²: CharZero RβR: Type u_1instβΒΉ: Semiring Rinstβ: CharZero Rq, n: βhn: n β  0βq ^ n = 1 β q = 1rw [Rβ: Type ?u.400instβΒ³: AddMonoidWithOne RβinstβΒ²: CharZero RβR: Type u_1instβΒΉ: Semiring Rinstβ: CharZero Rq, n: βhn: n β  0βq ^ n = 1 β q = 1β cast_pow: β {R : Type ?u.810} [inst : Semiring R] (n m : β), β(n ^ m) = βn ^ mcast_pow,Rβ: Type ?u.400instβΒ³: AddMonoidWithOne RβinstβΒ²: CharZero RβR: Type u_1instβΒΉ: Semiring Rinstβ: CharZero Rq, n: βhn: n β  0β(q ^ n) = 1 β q = 1 Rβ: Type ?u.400instβΒ³: AddMonoidWithOne RβinstβΒ²: CharZero RβR: Type u_1instβΒΉ: Semiring Rinstβ: CharZero Rq, 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 = 1cast_eq_oneRβ: Type ?u.400instβΒ³: AddMonoidWithOne RβinstβΒ²: CharZero RβR: Type u_1instβΒΉ: Semiring Rinstβ: CharZero Rq, n: βhn: n β  0q ^ n = 1 β q = 1]Rβ: Type ?u.400instβΒ³: AddMonoidWithOne RβinstβΒ²: CharZero RβR: Type u_1instβΒΉ: Semiring Rinstβ: CharZero Rq, n: βhn: n β  0q ^ n = 1 β q = 1
Rβ: Type ?u.400instβΒ³: AddMonoidWithOne RβinstβΒ²: CharZero RβR: Type u_1instβΒΉ: Semiring Rinstβ: CharZero Rq, 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 β  0hnGoals 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 / βncast_div_charZero {k: Type ?u.1363k : Type _: Type (?u.1363+1)Type _} [DivisionSemiring: Type ?u.1366 β Type ?u.1366DivisionSemiring k: Type ?u.1363k] [CharZero: (R : Type ?u.1369) β [inst : AddMonoidWithOne R] β PropCharZero k: Type ?u.1363k] {m: βm n: βn : β: Typeβ} (n_dvd: n β£ mn_dvd : n: βn β£ m: βm) :
((m: βm / n: βn : β: Typeβ) : k: Type ?u.1363k) = m: βm / n: βn := byGoals accomplished! π
R: Type ?u.1348instβΒ³: AddMonoidWithOne RinstβΒ²: CharZero Rk: Type u_1instβΒΉ: DivisionSemiring kinstβ: CharZero km, n: βn_dvd: n β£ mβ(m / n) = βm / βnrcases eq_or_ne: β {Ξ± : Sort ?u.2383} (x y : Ξ±), x = y β¨ x β  yeq_or_ne n: βn 0: ?m.23860 with (rfl | hn): n = 0 β¨ n β  0(rfl: n = 0rflrfl | hn: n = 0 β¨ n β  0 | hn: n β  0hn(rfl | hn): n = 0 β¨ n β  0)R: Type ?u.1348instβΒ³: AddMonoidWithOne RinstβΒ²: CharZero Rk: Type u_1instβΒΉ: DivisionSemiring kinstβ: CharZero km: βn_dvd: 0 β£ minlβ(m / 0) = βm / β0R: Type ?u.1348instβΒ³: AddMonoidWithOne RinstβΒ²: CharZero Rk: Type u_1instβΒΉ: DivisionSemiring kinstβ: CharZero km, n: βn_dvd: n β£ mhn: n β  0inrβ(m / n) = βm / βn
R: Type ?u.1348instβΒ³: AddMonoidWithOne RinstβΒ²: CharZero Rk: Type u_1instβΒΉ: DivisionSemiring kinstβ: CharZero km, n: βn_dvd: n β£ mβ(m / n) = βm / βnΒ·R: Type ?u.1348instβΒ³: AddMonoidWithOne RinstβΒ²: CharZero Rk: Type u_1instβΒΉ: DivisionSemiring kinstβ: CharZero km: βn_dvd: 0 β£ minlβ(m / 0) = βm / β0 R: Type ?u.1348instβΒ³: AddMonoidWithOne RinstβΒ²: CharZero Rk: Type u_1instβΒΉ: DivisionSemiring kinstβ: CharZero km: βn_dvd: 0 β£ minlβ(m / 0) = βm / β0R: Type ?u.1348instβΒ³: AddMonoidWithOne RinstβΒ²: CharZero Rk: Type u_1instβΒΉ: DivisionSemiring kinstβ: CharZero km, n: βn_dvd: n β£ mhn: n β  0inrβ(m / n) = βm / βnsimpGoals accomplished! π
R: Type ?u.1348instβΒ³: AddMonoidWithOne RinstβΒ²: CharZero Rk: Type u_1instβΒΉ: DivisionSemiring kinstβ: CharZero km, n: βn_dvd: n β£ mβ(m / n) = βm / βnΒ·R: Type ?u.1348instβΒ³: AddMonoidWithOne RinstβΒ²: CharZero Rk: Type u_1instβΒΉ: DivisionSemiring kinstβ: CharZero km, n: βn_dvd: n β£ mhn: n β  0inrβ(m / n) = βm / βn R: Type ?u.1348instβΒ³: AddMonoidWithOne RinstβΒ²: CharZero Rk: Type u_1instβΒΉ: DivisionSemiring kinstβ: CharZero km, n: βn_dvd: n β£ mhn: n β  0inrβ(m / n) = βm / βnexact cast_div: β {Ξ± : Type ?u.3093} [inst : DivisionSemiring Ξ±] {m n : β}, n β£ m β βn β  0 β β(m / n) = βm / βncast_div n_dvd: n β£ mn_dvd (cast_ne_zero: β {R : Type ?u.3119} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {n : β}, βn β  0 β n β  0cast_ne_zero.2: β {a b : Prop}, (a β b) β b β a2 hn: n β  0hn)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 / βnNat.cast_div_charZero

end Nat

section

variable (M: Type ?u.3310M : Type _: Type (?u.3310+1)Type _) [AddMonoidWithOne: Type ?u.3298 β Type ?u.3298AddMonoidWithOne M: Type ?u.3295M] [CharZero: (R : Type ?u.3301) β [inst : AddMonoidWithOne R] β PropCharZero M: Type ?u.3295M]

instance CharZero.NeZero.two: NeZero 2CharZero.NeZero.two : NeZero: {R : Type ?u.3325} β [inst : Zero R] β R β PropNeZero (2: ?m.33642 : M: Type ?u.3310M) :=
β¨byGoals accomplished! π
M: Type ?u.3310instβΒΉ: AddMonoidWithOne Minstβ: CharZero M2 β  0have : ((2: ?m.41312 : β: Typeβ) : M: Type ?u.3310M) β  0: ?m.43520 := Nat.cast_ne_zero: β {R : Type ?u.4758} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {n : β}, βn β  0 β n β  0Nat.cast_ne_zero.2: β {a b : Prop}, (a β b) β b β a2 (M: Type ?u.3310instβΒΉ: AddMonoidWithOne Minstβ: CharZero M2 β  0byGoals accomplished! π M: Type ?u.3310instβΒΉ: AddMonoidWithOne Minstβ: CharZero M2 β  0decideGoals accomplished! π)M: Type ?u.3310instβΒΉ: AddMonoidWithOne Minstβ: CharZero Mthis: β2 β  02 β  0
M: Type ?u.3310instβΒΉ: AddMonoidWithOne Minstβ: CharZero M2 β  0rwa [M: Type ?u.3310instβΒΉ: AddMonoidWithOne Minstβ: CharZero Mthis: β2 β  02 β  0Nat.cast_two: β {R : Type ?u.4830} [inst : AddMonoidWithOne R], β2 = 2Nat.cast_twoM: Type ?u.3310instβΒΉ: AddMonoidWithOne Minstβ: CharZero Mthis: 2 β  02 β  0]M: Type ?u.3310instβΒΉ: AddMonoidWithOne Minstβ: CharZero Mthis: 2 β  02 β  0 at this: β2 β  0thisGoals accomplished! πβ©
#align char_zero.ne_zero.two CharZero.NeZero.two: β (M : Type u_1) [inst : AddMonoidWithOne M] [inst_1 : CharZero M], NeZero 2CharZero.NeZero.two

end

section

variable {R: Type ?u.8459R : Type _: Type (?u.8459+1)Type _} [NonAssocSemiring: Type ?u.7436 β Type ?u.7436NonAssocSemiring R: Type ?u.4919R] [NoZeroDivisors: (Mβ : Type ?u.4925) β [inst : Mul Mβ] β [inst : Zero Mβ] β PropNoZeroDivisors R: Type ?u.8459R] [CharZero: (R : Type ?u.8856) β [inst : AddMonoidWithOne R] β PropCharZero R: Type ?u.5409R] {a: Ra : R: Type ?u.4919R}

@[simp]
theorem add_self_eq_zero: β {a : R}, a + a = 0 β a = 0add_self_eq_zero {a: Ra : R: Type ?u.5409R} : a: Ra + a: Ra = 0: ?m.59060 β a: Ra = 0: ?m.64290 := byGoals accomplished! π
R: Type u_1instβΒ²: NonAssocSemiring RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Raβ, a: Ra + a = 0 β a = 0simp only [(two_mul: β {Ξ± : Type ?u.6461} [inst : NonAssocSemiring Ξ±] (n : Ξ±), 2 * n = n + ntwo_mul a: Ra).symm: β {Ξ± : Sort ?u.6468} {a b : Ξ±}, a = b β b = asymm, mul_eq_zero: β {Mβ : Type ?u.6485} [inst : MulZeroClass Mβ] [inst_1 : NoZeroDivisors Mβ] {a b : Mβ}, a * b = 0 β a = 0 β¨ b = 0mul_eq_zero, two_ne_zero: β {Ξ± : Type ?u.6516} [inst : Zero Ξ±] [inst_1 : OfNat Ξ± 2] [inst_2 : NeZero 2], 2 β  0two_ne_zero, false_or_iff: β (p : Prop), False β¨ p β pfalse_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 = 0add_self_eq_zero

set_option linter.deprecated false

@[simp]
theorem bit0_eq_zero: β {a : R}, bit0 a = 0 β a = 0bit0_eq_zero {a: Ra : R: Type ?u.7433R} : bit0: {Ξ± : Type ?u.7926} β [inst : Add Ξ±] β Ξ± β Ξ±bit0 a: Ra = 0: ?m.80540 β a: Ra = 0: ?m.83390 :=
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 = 0add_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 = 0bit0_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 = 0zero_eq_bit0 {a: Ra : R: Type ?u.8459R} : 0: ?m.89530 = bit0: {Ξ± : Type ?u.8968} β [inst : Add Ξ±] β Ξ± β Ξ±bit0 a: Ra β a: Ra = 0: ?m.93700 := byGoals accomplished! π
R: Type u_1instβΒ²: NonAssocSemiring RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Raβ, a: R0 = bit0 a β a = 0rw [R: Type u_1instβΒ²: NonAssocSemiring RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Raβ, a: R0 = bit0 a β a = 0eq_comm: β {Ξ± : Sort ?u.9390} {a b : Ξ±}, a = b β b = aeq_commR: Type u_1instβΒ²: NonAssocSemiring RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Raβ, a: Rbit0 a = 0 β a = 0]R: Type u_1instβΒ²: NonAssocSemiring RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Raβ, a: Rbit0 a = 0 β a = 0
R: Type u_1instβΒ²: NonAssocSemiring RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Raβ, a: R0 = 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 = 0bit0_eq_zeroGoals 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 = 0zero_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 β  0bit0_ne_zero : bit0: {Ξ± : Type ?u.9994} β [inst : Add Ξ±] β Ξ± β Ξ±bit0 a: Ra β  0: ?m.101430 β a: Ra β  0: ?m.104150 :=
bit0_eq_zero: β {R : Type ?u.10418} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
bit0 a = 0 β a = 0bit0_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 β  0bit0_ne_zero

theorem zero_ne_bit0: 0 β  bit0 a β a β  0zero_ne_bit0 : 0: ?m.109860 β  bit0: {Ξ± : Type ?u.10996} β [inst : Add Ξ±] β Ξ± β Ξ±bit0 a: Ra β a: Ra β  0: ?m.111470 :=
zero_eq_bit0: β {R : Type ?u.11417} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
0 = bit0 a β a = 0zero_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 β  0zero_ne_bit0

end

section

variable {R: Type ?u.14297R : Type _: Type (?u.11497+1)Type _} [NonAssocRing: Type ?u.14300 β Type ?u.14300NonAssocRing R: Type ?u.18277R] [NoZeroDivisors: (Mβ : Type ?u.16745) β [inst : Mul Mβ] β [inst : Zero Mβ] β PropNoZeroDivisors R: Type ?u.11497R] [CharZero: (R : Type ?u.16103) β [inst : AddMonoidWithOne R] β PropCharZero R: Type ?u.11497R]

theorem neg_eq_self_iff: β {a : R}, -a = a β a = 0neg_eq_self_iff {a: Ra : R: Type ?u.11895R} : -a: Ra = a: Ra β a: Ra = 0: ?m.124060 :=
neg_eq_iff_add_eq_zero: β {G : Type ?u.12698} [inst : AddGroup G] {a b : G}, -a = b β a + b = 0neg_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 = 0add_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 = 0neg_eq_self_iff

theorem eq_neg_self_iff: β {a : R}, a = -a β a = 0eq_neg_self_iff {a: Ra : R: Type ?u.13096R} : a: Ra = -a: Ra β a: Ra = 0: ?m.136070 :=
eq_neg_iff_add_eq_zero: β {G : Type ?u.13899} [inst : AddGroup G] {a b : G}, a = -b β a + b = 0eq_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 = 0add_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 = 0eq_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 = bnat_mul_inj {n: βn : β: Typeβ} {a: Ra b: Rb : R: Type ?u.14297R} (h: βn * a = βn * bh : (n: βn : R: Type ?u.14297R) * a: Ra = (n: βn : R: Type ?u.14297R) * b: Rb) : n: βn = 0: ?m.150500 β¨ a: Ra = b: Rb := byGoals accomplished! π
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rh: βn * a = βn * bn = 0 β¨ a = brw [R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rh: βn * a = βn * bn = 0 β¨ a = bβ sub_eq_zero: β {G : Type ?u.15083} [inst : AddGroup G] {a b : G}, a - b = 0 β a = bsub_eq_zero,R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rhβ: βn * a = βn * bh: βn * a - βn * b = 0n = 0 β¨ a = b R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rh: βn * a = βn * bn = 0 β¨ a = bβ mul_sub: β {Ξ± : Type ?u.15221} [inst : NonUnitalNonAssocRing Ξ±] (a b c : Ξ±), a * (b - c) = a * b - a * cmul_sub,R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rhβ: βn * a = βn * bh: βn * (a - b) = 0n = 0 β¨ a = b R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rh: βn * a = βn * bn = 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 = 0mul_eq_zero,R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rhβ: βn * a = βn * bh: βn = 0 β¨ a - b = 0n = 0 β¨ a = b R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rh: βn * a = βn * bn = 0 β¨ a = bsub_eq_zero: β {G : Type ?u.15379} [inst : AddGroup G] {a b : G}, a - b = 0 β a = bsub_eq_zeroR: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rhβ: βn * a = βn * bh: βn = 0 β¨ a = bn = 0 β¨ a = b]R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rhβ: βn * a = βn * bh: βn = 0 β¨ a = bn = 0 β¨ a = b at h: βn = 0 β¨ a - b = 0hR: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rhβ: βn * a = βn * bh: βn = 0 β¨ a = bn = 0 β¨ a = b
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rh: βn * a = βn * bn = 0 β¨ a = bexact_mod_cast h: βn = 0 β¨ a = bhGoals 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 = bnat_mul_inj

theorem nat_mul_inj': β {n : β} {a b : R}, βn * a = βn * b β n β  0 β a = bnat_mul_inj' {n: βn : β: Typeβ} {a: Ra b: Rb : R: Type ?u.15782R} (h: βn * a = βn * bh : (n: βn : R: Type ?u.15782R) * a: Ra = (n: βn : R: Type ?u.15782R) * b: Rb) (w: n β  0w : n: βn β  0: ?m.165360) : a: Ra = b: Rb := byGoals accomplished! π
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Rn: βa, b: Rh: βn * a = βn * bw: n β  0a = bsimpa [w: n β  0w] 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 = bnat_mul_inj h: βn * a = βn * bhGoals 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 = bnat_mul_inj'

set_option linter.deprecated false

theorem bit0_injective: Function.Injective bit0bit0_injective : Function.Injective: {Ξ± : Sort ?u.17138} β {Ξ² : Sort ?u.17137} β (Ξ± β Ξ²) β PropFunction.Injective (bit0: {Ξ± : Type ?u.17144} β [inst : Add Ξ±] β Ξ± β Ξ±bit0 : R: Type ?u.16739R β R: Type ?u.16739R) := fun a: ?m.17204a b: ?m.17207b h: ?m.17210h => byGoals accomplished! π
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra, b: Rh: bit0 a = bit0 ba = bdsimp [bit0: {Ξ± : Type ?u.17217} β [inst : Add Ξ±] β Ξ± β Ξ±bit0] at h: bit0 a = bit0 bhR: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra, b: Rh: a + a = b + ba = b
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra, b: Rh: bit0 a = bit0 ba = bsimp only [(two_mul: β {Ξ± : Type ?u.17238} [inst : NonAssocSemiring Ξ±] (n : Ξ±), 2 * n = n + ntwo_mul a: Ra).symm: β {Ξ± : Sort ?u.17439} {a b : Ξ±}, a = b β b = asymm, (two_mul: β {Ξ± : Type ?u.17457} [inst : NonAssocSemiring Ξ±] (n : Ξ±), 2 * n = n + ntwo_mul b: Rb).symm: β {Ξ± : Sort ?u.17658} {a b : Ξ±}, a = b β b = asymm] at h: a + a = b + bhR: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra, b: Rh: 2 * a = 2 * ba = b
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra, b: Rh: bit0 a = bit0 ba = 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 = bnat_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 β  0two_ne_zeroR: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra, b: Rh: 2 * a = 2 * bβ2 * a = β2 * b
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra, b: Rh: bit0 a = bit0 ba = bexact_mod_cast h: 2 * a = 2 * bhGoals accomplished! π
#align bit0_injective bit0_injective: β {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R], Function.Injective bit0bit0_injective

theorem bit1_injective: Function.Injective bit1bit1_injective : Function.Injective: {Ξ± : Sort ?u.18676} β {Ξ² : Sort ?u.18675} β (Ξ± β Ξ²) β PropFunction.Injective (bit1: {Ξ± : Type ?u.18682} β [inst : One Ξ±] β [inst : Add Ξ±] β Ξ± β Ξ±bit1 : R: Type ?u.18277R β R: Type ?u.18277R) := fun a: ?m.18984a b: ?m.18987b h: ?m.18990h => byGoals accomplished! π
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra, b: Rh: bit1 a = bit1 ba = 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 = cadd_left_inj] at h: bit1 a = bit1 bhR: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra, b: Rh: bit0 a = bit0 ba = b
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra, b: Rh: bit1 a = bit1 ba = bexact bit0_injective: β {R : Type ?u.19294} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R], Function.Injective bit0bit0_injective h: bit0 a = bit0 bhGoals accomplished! π
#align bit1_injective bit1_injective: β {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R], Function.Injective bit1bit1_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 = bbit0_eq_bit0 {a: Ra b: Rb : R: Type ?u.19354R} : bit0: {Ξ± : Type ?u.19757} β [inst : Add Ξ±] β Ξ± β Ξ±bit0 a: Ra = bit0: {Ξ± : Type ?u.19790} β [inst : Add Ξ±] β Ξ± β Ξ±bit0 b: Rb β a: Ra = b: Rb :=
bit0_injective: β {R : Type ?u.19799} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R], Function.Injective bit0bit0_injective.eq_iff: β {Ξ± : Sort ?u.19823} {Ξ² : Sort ?u.19824} {f : Ξ± β Ξ²}, Function.Injective f β β {a b : Ξ±}, f a = f b β a = beq_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 = bbit0_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 = bbit1_eq_bit1 {a: Ra b: Rb : R: Type ?u.19924R} : bit1: {Ξ± : Type ?u.20327} β [inst : One Ξ±] β [inst : Add Ξ±] β Ξ± β Ξ±bit1 a: Ra = bit1: {Ξ± : Type ?u.20569} β [inst : One Ξ±] β [inst : Add Ξ±] β Ξ± β Ξ±bit1 b: Rb β a: Ra = b: Rb :=
bit1_injective: β {R : Type ?u.20579} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R], Function.Injective bit1bit1_injective.eq_iff: β {Ξ± : Sort ?u.20603} {Ξ² : Sort ?u.20604} {f : Ξ± β Ξ²}, Function.Injective f β β {a b : Ξ±}, f a = f b β a = beq_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 = bbit1_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 = 0bit1_eq_one {a: Ra : R: Type ?u.20700R} : bit1: {Ξ± : Type ?u.21101} β [inst : One Ξ±] β [inst : Add Ξ±] β Ξ± β Ξ±bit1 a: Ra = 1: ?m.213441 β a: Ra = 0: ?m.215340 := byGoals accomplished! π
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra: Rbit1 a = 1 β a = 0rw [R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra: Rbit1 a = 1 β a = 0show (1: ?m.218061 : R: Type u_1R) = bit1: {Ξ± : Type ?u.22026} β [inst : One Ξ±] β [inst : Add Ξ±] β Ξ± β Ξ±bit1 0: ?m.220310 by R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra: Rbit1 a = 1 β a = 0simpGoals accomplished! π,R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra: Rbit1 a = bit1 0 β a = 0 R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra: Rbit1 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 = bbit1_eq_bit1R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra: Ra = 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 = 0bit1_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 = 0one_eq_bit1 {a: Ra : R: Type ?u.22857R} : 1: ?m.232591 = bit1: {Ξ± : Type ?u.23274} β [inst : One Ξ±] β [inst : Add Ξ±] β Ξ± β Ξ±bit1 a: Ra β a: Ra = 0: ?m.236960 := byGoals accomplished! π
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra: R1 = bit1 a β a = 0rw [R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra: R1 = bit1 a β a = 0eq_comm: β {Ξ± : Sort ?u.23964} {a b : Ξ±}, a = b β b = aeq_commR: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra: Rbit1 a = 1 β a = 0]R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra: Rbit1 a = 1 β a = 0
R: Type u_1instβΒ²: NonAssocRing RinstβΒΉ: NoZeroDivisors Rinstβ: CharZero Ra: R1 = 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 = 0bit1_eq_oneGoals 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 = 0one_eq_bit1

end

section

variable {R: Type ?u.24072R : Type _: Type (?u.24072+1)Type _} [DivisionRing: Type ?u.25453 β Type ?u.25453DivisionRing R: Type ?u.24072R] [CharZero: (R : Type ?u.24078) β [inst : AddMonoidWithOne R] β PropCharZero R: Type ?u.24072R]

@[simp]
theorem half_add_self: β {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), (a + a) / 2 = ahalf_add_self (a: Ra : R: Type ?u.24147R) : (a: Ra + a: Ra) / 2: ?m.242322 = a: Ra := byGoals accomplished! π R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: R(a + a) / 2 = arw [R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: R(a + a) / 2 = aβ mul_two: β {Ξ± : Type ?u.24669} [inst : NonAssocSemiring Ξ±] (n : Ξ±), n * 2 = n + nmul_two,R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra * 2 / 2 = a R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: R(a + a) / 2 = amul_div_cancel: β {Gβ : Type ?u.24859} [inst : GroupWithZero Gβ] {b : Gβ} (a : Gβ), b β  0 β a * b / b = amul_div_cancel a: Ra two_ne_zero: β {Ξ± : Type ?u.24863} [inst : Zero Ξ±] [inst_1 : OfNat Ξ± 2] [inst_2 : NeZero 2], 2 β  0two_ne_zeroR: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra = 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 = ahalf_add_self

@[simp]
theorem add_halves': β {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a / 2 + a / 2 = aadd_halves' (a: Ra : R: Type ?u.25450R) : a: Ra / 2: ?m.255352 + a: Ra / 2: ?m.255482 = a: Ra := byGoals accomplished! π R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra / 2 + a / 2 = arw [R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra / 2 + a / 2 = aβ add_div: β {Ξ± : Type ?u.26046} [inst : DivisionSemiring Ξ±] (a b c : Ξ±), (a + b) / c = a / c + b / cadd_div,R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: R(a + a) / 2 = a R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra / 2 + a / 2 = ahalf_add_self: β {R : Type ?u.26118} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), (a + a) / 2 = ahalf_add_selfR: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra = 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 = aadd_halves'

theorem sub_half: β {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a - a / 2 = a / 2sub_half (a: Ra : R: Type ?u.26193R) : a: Ra - a: Ra / 2: ?m.262782 = a: Ra / 2: ?m.262952 := byGoals accomplished! π R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra - a / 2 = a / 2rw [R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra - a / 2 = a / 2sub_eq_iff_eq_add: β {G : Type ?u.26753} [inst : AddGroup G] {a b c : G}, a - b = c β a = c + bsub_eq_iff_eq_add,R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra = a / 2 + a / 2 R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra - a / 2 = a / 2add_halves': β {R : Type ?u.26859} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a / 2 + a / 2 = aadd_halves'R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra = 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 / 2sub_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: Ra : R: Type ?u.26933R) : a: Ra / 2: ?m.270182 - a: Ra = -(a: Ra / 2: ?m.270362) := byGoals accomplished! π R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra / 2 - a = -(a / 2)rw [R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra / 2 - a = -(a / 2)β neg_sub: β {Ξ± : Type ?u.27544} [inst : SubtractionMonoid Ξ±] (a b : Ξ±), -(a - b) = b - aneg_sub,R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: R-(a - a / 2) = -(a / 2) R: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: Ra / 2 - a = -(a / 2)sub_half: β {R : Type ?u.27667} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a - a / 2 = a / 2sub_halfR: Type u_1instβΒΉ: DivisionRing Rinstβ: CharZero Ra: 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.27736R : Type _: Type (?u.27736+1)Type _} [AddMonoidWithOne: Type ?u.27739 β Type ?u.27739AddMonoidWithOne R: Type ?u.27736R] [CharZero: (R : Type ?u.27742) β [inst : AddMonoidWithOne R] β PropCharZero R: Type ?u.27736R] :
CharZero: (R : Type ?u.27751) β [inst : AddMonoidWithOne R] β PropCharZero (WithTop: Type ?u.27752 β Type ?u.27752WithTop R: Type ?u.27736R) where
cast_injective m: ?m.27782m n: ?m.27785n h: ?m.27788h := byGoals accomplished! π

end WithTop

section RingHom

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

theorem RingHom.charZero: β {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
(R β+* S) β β [hS : CharZero S], CharZero RRingHom.charZero (Ο: R β+* SΟ : R: Type ?u.28015R β+* S: Type ?u.28018S) [hS: CharZero ShS : CharZero: (R : Type ?u.28043) β [inst : AddMonoidWithOne R] β PropCharZero S: Type ?u.28018S] : CharZero: (R : Type ?u.28157) β [inst : AddMonoidWithOne R] β PropCharZero R: Type ?u.28015R :=
β¨fun a: ?m.28294a b: ?m.28297b h: ?m.28300h => CharZero.cast_injective: β {R : Type ?u.28302} [inst : AddMonoidWithOne R] [self : CharZero R], Function.Injective Nat.castCharZero.cast_injective (byGoals accomplished! π R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShS: CharZero Sa, b: βh: βa = βbβa = βbrw [R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShS: CharZero Sa, 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 = βnmap_natCast Ο: R β+* SΟ,R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShS: CharZero Sa, b: βh: βa = βbβΟ βa = βb R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShS: CharZero Sa, 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 = βnmap_natCast Ο: R β+* SΟ,R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShS: CharZero Sa, b: βh: βa = βbβΟ βa = βΟ βb R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShS: CharZero Sa, b: βh: βa = βbβa = βbh: βa = βbhR: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShS: CharZero Sa, 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 RRingHom.charZero

theorem RingHom.charZero_iff: β {Ο : R β+* S}, Function.Injective βΟ β (CharZero R β CharZero S)RingHom.charZero_iff {Ο: R β+* SΟ : R: Type ?u.29119R β+* S: Type ?u.29122S} (hΟ: Function.Injective βΟhΟ : Function.Injective: {Ξ± : Sort ?u.29148} β {Ξ² : Sort ?u.29147} β (Ξ± β Ξ²) β PropFunction.Injective Ο: R β+* SΟ) : CharZero: (R : Type ?u.29430) β [inst : AddMonoidWithOne R] β PropCharZero R: Type ?u.29119R β CharZero: (R : Type ?u.29541) β [inst : AddMonoidWithOne R] β PropCharZero S: Type ?u.29122S :=
β¨fun hR: ?m.29664hR =>
β¨byGoals accomplished! π R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero RFunction.Injective Nat.castintro a: βa b: βb h: βa = βbhR: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero Ra, b: βh: βa = βba = b;R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero Ra, b: βh: βa = βba = b R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero RFunction.Injective Nat.castrwa [R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero Ra, b: βh: βa = βba = bβ @Nat.cast_inj: β {R : Type ?u.29846} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {m n : β}, βm = βn β m = nNat.cast_inj R: Type u_1R,R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero Ra, b: βh: βa = βbβa = βb R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero Ra, b: βh: βa = βba = bβ hΟ: Function.Injective βΟhΟ.eq_iff: β {Ξ± : Sort ?u.29967} {Ξ² : Sort ?u.29968} {f : Ξ± β Ξ²}, Function.Injective f β β {a b : Ξ±}, f a = f b β a = beq_iff,R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero Ra, b: βh: βa = βbβΟ βa = βΟ βb R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero Ra, b: βh: βa = βba = 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 = βnmap_natCast Ο: R β+* SΟ,R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero Ra, b: βh: βa = βbβa = βΟ βb R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero Ra, b: βh: βa = βba = 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 = βnmap_natCast Ο: R β+* SΟR: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero Ra, b: βh: βa = βbβa = βb]R: Type u_1S: Type u_2instβΒΉ: NonAssocSemiring Rinstβ: NonAssocSemiring SΟ: R β+* ShΟ: Function.Injective βΟhR: CharZero Ra, b: βh: βa = βbβa = βbβ©,
fun hS: ?m.29803hS => Ο: R β+* SΟ.charZero: β {R : Type ?u.29805} {S : Type ?u.29806} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
(R β+* S) β β [hS : CharZero S], CharZero RcharZeroβ©
#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 βfRingHom.injective_nat (f: β β+* Rf : β: Typeβ β+* R: Type ?u.30168R) [CharZero: (R : Type ?u.30206) β [inst : AddMonoidWithOne R] β PropCharZero R: Type ?u.30168R] : Function.Injective: {Ξ± : Sort ?u.30321} β {Ξ² : Sort ?u.30320} β (Ξ± β Ξ²) β PropFunction.Injective f: β β+* Rf :=
Subsingleton.elim: β {Ξ± : Sort ?u.30594} [h : Subsingleton Ξ±] (a b : Ξ±), a = bSubsingleton.elim (Nat.castRingHom: (Ξ± : Type ?u.30597) β [inst : NonAssocSemiring Ξ±] β β β+* Ξ±Nat.castRingHom _: Type ?u.30597_) f: β β+* Rf βΈ Nat.cast_injective: β {R : Type ?u.30634} [inst : AddMonoidWithOne R] [inst_1 : CharZero R], Function.Injective Nat.castNat.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 βfRingHom.injective_nat

end RingHom
```