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 data.nat.cast.basic
! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.CharZero.Defs
import Mathlib.Algebra.GroupWithZero.Commute
import Mathlib.Algebra.Hom.Ring
import Mathlib.Algebra.Order.Group.Abs
import Mathlib.Algebra.Ring.Commute
import Mathlib.Data.Nat.Order.Basic
import Mathlib.Algebra.Group.Opposite

/-!
# Cast of natural numbers (additional theorems)

This file proves additional properties about the *canonical* homomorphism from
the natural numbers into an additive monoid with a one (`Nat.cast`).

## Main declarations

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

-- Porting note: There are many occasions below where we need `simp [map_zero f]`
-- where `simp [map_zero]` should suffice. (Similarly for `map_one`.)
-- See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20regression.20with.20MonoidHomClass

variable {
α: Type ?u.33331
α
β: Type ?u.11
β
:
Type _: Type (?u.6990+1)
Type _
} namespace Nat /-- `Nat.cast : ℕ → α` as an `AddMonoidHom`. -/ def
castAddMonoidHom: (α : Type u_1) → [inst : AddMonoidWithOne α] → →+ α
castAddMonoidHom
(
α: Type ?u.14
α
:
Type _: Type (?u.14+1)
Type _
) [
AddMonoidWithOne: Type ?u.17 → Type ?u.17
AddMonoidWithOne
α: Type ?u.14
α
] :
: Type
→+
α: Type ?u.14
α
where toFun :=
Nat.cast: {R : Type ?u.566} → [inst : NatCast R] → R
Nat.cast
map_add' :=
cast_add: ∀ {R : Type ?u.743} [inst : AddMonoidWithOne R] (m n : ), ↑(m + n) = m + n
cast_add
map_zero' :=
cast_zero: ∀ {R : Type ?u.725} [inst : AddMonoidWithOne R], 0 = 0
cast_zero
#align nat.cast_add_monoid_hom
Nat.castAddMonoidHom: (α : Type u_1) → [inst : AddMonoidWithOne α] → →+ α
Nat.castAddMonoidHom
@[simp] theorem
coe_castAddMonoidHom: ∀ {α : Type u_1} [inst : AddMonoidWithOne α], ↑(castAddMonoidHom α) = Nat.cast
coe_castAddMonoidHom
[
AddMonoidWithOne: Type ?u.824 → Type ?u.824
AddMonoidWithOne
α: Type ?u.818
α
] : (
castAddMonoidHom: (α : Type ?u.831) → [inst : AddMonoidWithOne α] → →+ α
castAddMonoidHom
α: Type ?u.818
α
:
: Type
α: Type ?u.818
α
) =
Nat.cast: {R : Type ?u.1820} → [inst : NatCast R] → R
Nat.cast
:=
rfl: ∀ {α : Sort ?u.2066} {a : α}, a = a
rfl
#align nat.coe_cast_add_monoid_hom
Nat.coe_castAddMonoidHom: ∀ {α : Type u_1} [inst : AddMonoidWithOne α], ↑(castAddMonoidHom α) = Nat.cast
Nat.coe_castAddMonoidHom
@[simp, norm_cast] theorem
cast_mul: ∀ [inst : NonAssocSemiring α] (m n : ), ↑(m * n) = m * n
cast_mul
[
NonAssocSemiring: Type ?u.2103 → Type ?u.2103
NonAssocSemiring
α: Type ?u.2097
α
] (
m:
m
n:
n
:
: Type
) : ((
m:
m
*
n:
n
:
: Type
) :
α: Type ?u.2097
α
) =
m:
m
*
n:
n
:=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m, n:


↑(m * n) = m * n
α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m:


zero
↑(m * zero) = m * zero
α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m, n✝:

n_ih✝: ↑(m * n✝) = m * n✝


succ
↑(m * succ n✝) = m * ↑(succ n✝)
α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m, n:


↑(m * n) = m * n
α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m:


zero
↑(m * zero) = m * zero
α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m, n✝:

n_ih✝: ↑(m * n✝) = m * n✝


succ
↑(m * succ n✝) = m * ↑(succ n✝)
α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m, n:


↑(m * n) = m * n

Goals accomplished! 🐙
#align nat.cast_mul
Nat.cast_mul: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (m n : ), ↑(m * n) = m * n
Nat.cast_mul
/-- `Nat.cast : ℕ → α` as a `RingHom` -/ def
castRingHom: (α : Type u_1) → [inst : NonAssocSemiring α] → →+* α
castRingHom
(
α: Type ?u.4477
α
:
Type _: Type (?u.4477+1)
Type _
) [
NonAssocSemiring: Type ?u.4480 → Type ?u.4480
NonAssocSemiring
α: Type ?u.4477
α
] :
: Type
→+*
α: Type ?u.4477
α
:= {
castAddMonoidHom: (α : Type ?u.4511) → [inst : AddMonoidWithOne α] → →+ α
castAddMonoidHom
α: Type ?u.4477
α
with toFun :=
Nat.cast: {R : Type ?u.4854} → [inst : NatCast R] → R
Nat.cast
, map_one' :=
cast_one: ∀ {R : Type ?u.4997} [inst : AddMonoidWithOne R], 1 = 1
cast_one
, map_mul' :=
cast_mul: ∀ {α : Type ?u.5014} [inst : NonAssocSemiring α] (m n : ), ↑(m * n) = m * n
cast_mul
} #align nat.cast_ring_hom
Nat.castRingHom: (α : Type u_1) → [inst : NonAssocSemiring α] → →+* α
Nat.castRingHom
@[simp] theorem
coe_castRingHom: ∀ {α : Type u_1} [inst : NonAssocSemiring α], ↑(castRingHom α) = Nat.cast
coe_castRingHom
[
NonAssocSemiring: Type ?u.5452 → Type ?u.5452
NonAssocSemiring
α: Type ?u.5446
α
] : (
castRingHom: (α : Type ?u.5459) → [inst : NonAssocSemiring α] → →+* α
castRingHom
α: Type ?u.5446
α
:
: Type
α: Type ?u.5446
α
) =
Nat.cast: {R : Type ?u.5996} → [inst : NatCast R] → R
Nat.cast
:=
rfl: ∀ {α : Sort ?u.6222} {a : α}, a = a
rfl
#align nat.coe_cast_ring_hom
Nat.coe_castRingHom: ∀ {α : Type u_1} [inst : NonAssocSemiring α], ↑(castRingHom α) = Nat.cast
Nat.coe_castRingHom
theorem
cast_commute: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ) (x : α), Commute (n) x
cast_commute
[
NonAssocSemiring: Type ?u.6259 → Type ?u.6259
NonAssocSemiring
α: Type ?u.6253
α
] (
n:
n
:
: Type
) (
x: α
x
:
α: Type ?u.6253
α
) :
Commute: {S : Type ?u.6266} → [inst : Mul S] → SSProp
Commute
(
n:
n
:
α: Type ?u.6253
α
)
x: α
x
:=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

n:

x: α


Commute (n) x
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

n:

x: α


Commute (n) x
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α


zero
Commute (zero) x
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α


zero
Commute (zero) x
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α


zero
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α


zero
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α


zero
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α


zero
Commute (zero) x

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

n:

x: α


Commute (n) x
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n:

ihn: Commute (n) x


succ
Commute (↑(succ n)) x
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n:

ihn: Commute (n) x


succ
Commute (↑(succ n)) x
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n:

ihn: Commute (n) x


succ
Commute (n + 1) x
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n:

ihn: Commute (n) x


succ
Commute (n + 1) x
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n:

ihn: Commute (n) x


succ
Commute (n + 1) x
α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n:

ihn: Commute (n) x


succ
Commute (↑(succ n)) x

Goals accomplished! 🐙
#align nat.cast_commute
Nat.cast_commute: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ) (x : α), Commute (n) x
Nat.cast_commute
theorem
cast_comm: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ) (x : α), n * x = x * n
cast_comm
[
NonAssocSemiring: Type ?u.6996 → Type ?u.6996
NonAssocSemiring
α: Type ?u.6990
α
] (
n:
n
:
: Type
) (
x: α
x
:
α: Type ?u.6990
α
) : (
n:
n
:
α: Type ?u.6990
α
) *
x: α
x
=
x: α
x
*
n:
n
:= (
cast_commute: ∀ {α : Type ?u.7644} [inst : NonAssocSemiring α] (n : ) (x : α), Commute (n) x
cast_commute
n:
n
x: α
x
).
eq: ∀ {S : Type ?u.7651} [inst : Mul S] {a b : S}, Commute a ba * b = b * a
eq
#align nat.cast_comm
Nat.cast_comm: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ) (x : α), n * x = x * n
Nat.cast_comm
theorem
commute_cast: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (x : α) (n : ), Commute x n
commute_cast
[
NonAssocSemiring: Type ?u.7783 → Type ?u.7783
NonAssocSemiring
α: Type ?u.7777
α
] (
x: α
x
:
α: Type ?u.7777
α
) (
n:
n
:
: Type
) :
Commute: {S : Type ?u.7790} → [inst : Mul S] → SSProp
Commute
x: α
x
n:
n
:= (
n:
n
.
cast_commute: ∀ {α : Type ?u.8103} [inst : NonAssocSemiring α] (n : ) (x : α), Commute (n) x
cast_commute
x: α
x
).
symm: ∀ {S : Type ?u.8114} [inst : Mul S] {a b : S}, Commute a bCommute b a
symm
#align nat.commute_cast
Nat.commute_cast: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (x : α) (n : ), Commute x n
Nat.commute_cast
section OrderedSemiring variable [
OrderedSemiring: Type ?u.13765 → Type ?u.13765
OrderedSemiring
α: Type ?u.13759
α
] @[mono] theorem
mono_cast: Monotone Nat.cast
mono_cast
:
Monotone: {α : Type ?u.8256} → {β : Type ?u.8255} → [inst : Preorder α] → [inst : Preorder β] → (αβ) → Prop
Monotone
(
Nat.cast: {R : Type ?u.8296} → [inst : NatCast R] → R
Nat.cast
:
: Type
α: Type ?u.8246
α
) :=
monotone_nat_of_le_succ: ∀ {α : Type ?u.8523} [inst : Preorder α] {f : α}, (∀ (n : ), f n f (n + 1)) → Monotone f
monotone_nat_of_le_succ
fun
n: ?m.8577
n

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n:


n ↑(n + 1)
α: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n:


n ↑(n + 1)
α: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n:


n n + 1
α: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n:


n n + 1
α: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n:


n n + 1
α: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n:


n ↑(n + 1)

Goals accomplished! 🐙
#align nat.mono_cast
Nat.mono_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α], Monotone Nat.cast
Nat.mono_cast
@[simp] theorem
cast_nonneg: ∀ {α : Type u_1} [inst : OrderedSemiring α] (n : ), 0 n
cast_nonneg
(
n:
n
:
: Type
) :
0: ?m.9719
0
≤ (
n:
n
:
α: Type ?u.9706
α
) := @
Nat.cast_zero: ∀ {R : Type ?u.10082} [inst : AddMonoidWithOne R], 0 = 0
Nat.cast_zero
α: Type ?u.9706
α
_ ▸
mono_cast: ∀ {α : Type ?u.10225} [inst : OrderedSemiring α], Monotone Nat.cast
mono_cast
(
Nat.zero_le: ∀ (n : ), 0 n
Nat.zero_le
n:
n
) #align nat.cast_nonneg
Nat.cast_nonneg: ∀ {α : Type u_1} [inst : OrderedSemiring α] (n : ), 0 n
Nat.cast_nonneg
section Nontrivial variable [
Nontrivial: Type ?u.10295 → Prop
Nontrivial
α: Type ?u.10286
α
] theorem
cast_add_one_pos: ∀ (n : ), 0 < n + 1
cast_add_one_pos
(
n:
n
:
: Type
) :
0: ?m.10314
0
< (
n:
n
:
α: Type ?u.10298
α
) +
1: ?m.10445
1
:=
zero_lt_one: ∀ {α : Type ?u.11032} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α] [inst_4 : NeZero 1], 0 < 1
zero_lt_one
.
trans_le: ∀ {α : Type ?u.11342} [inst : Preorder α] {a b c : α}, a < bb ca < c
trans_le
<|
le_add_of_nonneg_left: ∀ {α : Type ?u.11522} [inst : AddZeroClass α] [inst_1 : LE α] [inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a b : α}, 0 ba b + a
le_add_of_nonneg_left
n:
n
.
cast_nonneg: ∀ {α : Type ?u.11728} [inst : OrderedSemiring α] (n : ), 0 n
cast_nonneg
#align nat.cast_add_one_pos
Nat.cast_add_one_pos: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] (n : ), 0 < n + 1
Nat.cast_add_one_pos
@[simp] theorem
cast_pos: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] {n : }, 0 < n 0 < n
cast_pos
{
n:
n
:
: Type
} : (
0: ?m.12335
0
:
α: Type ?u.12318
α
) <
n:
n
0: ?m.12762
0
<
n:
n
:=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

n:


0 < n 0 < n
α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α


zero
0 < zero 0 < zero
α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

n✝:


succ
0 < ↑(succ n✝) 0 < succ n✝
α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

n:


0 < n 0 < n
α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α


zero
0 < zero 0 < zero
α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

n✝:


succ
0 < ↑(succ n✝) 0 < succ n✝
α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

n:


0 < n 0 < n

Goals accomplished! 🐙
#align nat.cast_pos
Nat.cast_pos: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] {n : }, 0 < n 0 < n
Nat.cast_pos
end Nontrivial variable [
CharZero: (R : Type ?u.15455) → [inst : AddMonoidWithOne R] → Prop
CharZero
α: Type ?u.13759
α
] {
m:
m
n:
n
:
: Type
} theorem
strictMono_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α], StrictMono Nat.cast
strictMono_cast
:
StrictMono: {α : Type ?u.14076} → {β : Type ?u.14075} → [inst : Preorder α] → [inst : Preorder β] → (αβ) → Prop
StrictMono
(
Nat.cast: {R : Type ?u.14116} → [inst : NatCast R] → R
Nat.cast
:
: Type
α: Type ?u.13917
α
) :=
mono_cast: ∀ {α : Type ?u.14343} [inst : OrderedSemiring α], Monotone Nat.cast
mono_cast
.
strictMono_of_injective: ∀ {α : Type ?u.14352} {β : Type ?u.14351} [inst : Preorder α] [inst_1 : PartialOrder β] {f : αβ}, Monotone fFunction.Injective fStrictMono f
strictMono_of_injective
cast_injective: ∀ {R : Type ?u.14458} [inst : AddMonoidWithOne R] [inst_1 : CharZero R], Function.Injective Nat.cast
cast_injective
#align nat.strict_mono_cast
Nat.strictMono_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α], StrictMono Nat.cast
Nat.strictMono_cast
/-- `Nat.cast : ℕ → α` as an `OrderEmbedding` -/ @[simps! (config := { fullyApplied :=
false: Bool
false
})] def
castOrderEmbedding: ↪o α
castOrderEmbedding
:
: Type
↪o
α: Type ?u.14695
α
:=
OrderEmbedding.ofStrictMono: {α : Type ?u.14965} → {β : Type ?u.14964} → [inst : LinearOrder α] → [inst_1 : Preorder β] → (f : αβ) → StrictMono fα ↪o β
OrderEmbedding.ofStrictMono
Nat.cast: {R : Type ?u.15095} → [inst : NatCast R] → R
Nat.cast
Nat.strictMono_cast: ∀ {α : Type ?u.15174} [inst : OrderedSemiring α] [inst_1 : CharZero α], StrictMono Nat.cast
Nat.strictMono_cast
#align nat.cast_order_embedding
Nat.castOrderEmbedding: {α : Type u_1} → [inst : OrderedSemiring α] → [inst_1 : CharZero α] → ↪o α
Nat.castOrderEmbedding
#align nat.cast_order_embedding_apply
Nat.castOrderEmbedding_apply: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α], castOrderEmbedding = Nat.cast
Nat.castOrderEmbedding_apply
@[simp, norm_cast] theorem
cast_le: m n m n
cast_le
: (
m:
m
:
α: Type ?u.15446
α
) ≤
n:
n
m:
m
n:
n
:=
strictMono_cast: ∀ {α : Type ?u.15979} [inst : OrderedSemiring α] [inst_1 : CharZero α], StrictMono Nat.cast
strictMono_cast
.
le_iff_le: ∀ {α : Type ?u.15992} {β : Type ?u.15991} [inst : LinearOrder α] [inst_1 : Preorder β] {f : αβ}, StrictMono f∀ {a b : α}, f a f b a b
le_iff_le
#align nat.cast_le
Nat.cast_le: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {m n : }, m n m n
Nat.cast_le
@[simp, norm_cast, mono] theorem
cast_lt: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {m n : }, m < n m < n
cast_lt
: (
m:
m
:
α: Type ?u.16299
α
) <
n:
n
m:
m
<
n:
n
:=
strictMono_cast: ∀ {α : Type ?u.16832} [inst : OrderedSemiring α] [inst_1 : CharZero α], StrictMono Nat.cast
strictMono_cast
.
lt_iff_lt: ∀ {α : Type ?u.16845} {β : Type ?u.16844} [inst : LinearOrder α] [inst_1 : Preorder β] {f : αβ}, StrictMono f∀ {a b : α}, f a < f b a < b
lt_iff_lt
#align nat.cast_lt
Nat.cast_lt: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {m n : }, m < n m < n
Nat.cast_lt
@[simp, norm_cast] theorem
one_lt_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {n : }, 1 < n 1 < n
one_lt_cast
:
1: ?m.17312
1
< (
n:
n
:
α: Type ?u.17152
α
) ↔
1: ?m.17609
1
<
n:
n
:=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.17155

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


1 < n 1 < n
α: Type u_1

β: Type ?u.17155

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


1 < n 1 < n
α: Type u_1

β: Type ?u.17155

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


1 < n 1 < n
α: Type u_1

β: Type ?u.17155

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


1 < n 1 < n
α: Type u_1

β: Type ?u.17155

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


1 < n 1 < n

Goals accomplished! 🐙
#align nat.one_lt_cast
Nat.one_lt_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {n : }, 1 < n 1 < n
Nat.one_lt_cast
@[simp, norm_cast] theorem
one_le_cast: 1 n 1 n
one_le_cast
:
1: ?m.18162
1
≤ (
n:
n
:
α: Type ?u.18002
α
) ↔
1: ?m.18459
1
n:
n
:=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.18005

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


1 n 1 n
α: Type u_1

β: Type ?u.18005

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


1 n 1 n
α: Type u_1

β: Type ?u.18005

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


1 n 1 n
α: Type u_1

β: Type ?u.18005

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


1 n 1 n
α: Type u_1

β: Type ?u.18005

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


1 n 1 n

Goals accomplished! 🐙
#align nat.one_le_cast
Nat.one_le_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {n : }, 1 n 1 n
Nat.one_le_cast
@[simp, norm_cast] theorem
cast_lt_one: n < 1 n = 0
cast_lt_one
: (
n:
n
:
α: Type ?u.18852
α
) <
1: ?m.19124
1
n:
n
=
0: ?m.19304
0
:=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n < 1 n = 0
α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n < 1 n = 0
α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n < 1 n = 0
α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n < 1 n = 0
α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n < 1 n = 0
α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n < 1 n = 0
α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n 0 n = 0
α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n < 1 n = 0
α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n < 1 n = 0
α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n = n =

Goals accomplished! 🐙
#align nat.cast_lt_one
Nat.cast_lt_one: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {n : }, n < 1 n = 0
Nat.cast_lt_one
@[simp, norm_cast] theorem
cast_le_one: n 1 n 1
cast_le_one
: (
n:
n
:
α: Type ?u.19890
α
) ≤
1: ?m.20162
1
n:
n
1: ?m.20342
1
:=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.19893

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n 1 n 1
α: Type u_1

β: Type ?u.19893

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n 1 n 1
α: Type u_1

β: Type ?u.19893

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n 1 n 1
α: Type u_1

β: Type ?u.19893

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n 1 n 1
α: Type u_1

β: Type ?u.19893

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n:


n 1 n 1

Goals accomplished! 🐙
#align nat.cast_le_one
Nat.cast_le_one: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {n : }, n 1 n 1
Nat.cast_le_one
end OrderedSemiring /-- A version of `Nat.cast_sub` that works for `ℝ≥0` and `ℚ≥0`. Note that this proof doesn't work for `ℕ∞` and `ℝ≥0∞`, so we use type-specific lemmas for these types. -/ @[simp, norm_cast] theorem
cast_tsub: ∀ {α : Type u_1} [inst : CanonicallyOrderedCommSemiring α] [inst_1 : Sub α] [inst_2 : OrderedSub α] [inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (m n : ), ↑(m - n) = m - n
cast_tsub
[
CanonicallyOrderedCommSemiring: Type ?u.20733 → Type ?u.20733
CanonicallyOrderedCommSemiring
α: Type ?u.20727
α
] [
Sub: Type ?u.20736 → Type ?u.20736
Sub
α: Type ?u.20727
α
] [
OrderedSub: (α : Type ?u.20739) → [inst : LE α] → [inst : Add α] → [inst : Sub α] → Prop
OrderedSub
α: Type ?u.20727
α
] [
ContravariantClass: (M : Type ?u.21006) → (N : Type ?u.21005) → (MNN) → (NNProp) → Prop
ContravariantClass
α: Type ?u.20727
α
α: Type ?u.20727
α
(· + ·): ααα
(· + ·)
(· ≤ ·): ααProp
(· ≤ ·)
] (
m:
m
n:
n
:
: Type
) : ↑(
m:
m
-
n:
n
) = (
m:
m
-
n:
n
:
α: Type ?u.20727
α
) :=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:


↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: n m


inr
↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:


↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: n m


inr
↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
0 = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
0 = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
0 = 0
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
m n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
m n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: m n


inl
↑(m - n) = m - n

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:


↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: n m


inr
↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: n m


inr
↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

n, m:

h: n m + n


inr.intro
↑(m + n - n) = ↑(m + n) - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

m, n:

h: n m


inr
↑(m - n) = m - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

n, m:

h: n m + n


inr.intro
↑(m + n - n) = ↑(m + n) - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

n, m:

h: n m + n


inr.intro
m = ↑(m + n) - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

n, m:

h: n m + n


inr.intro
↑(m + n - n) = ↑(m + n) - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

n, m:

h: n m + n


inr.intro
m = m + n - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

n, m:

h: n m + n


inr.intro
↑(m + n - n) = ↑(m + n) - n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1

n, m:

h: n m + n


inr.intro
m = m

Goals accomplished! 🐙
#align nat.cast_tsub
Nat.cast_tsub: ∀ {α : Type u_1} [inst : CanonicallyOrderedCommSemiring α] [inst_1 : Sub α] [inst_2 : OrderedSub α] [inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (m n : ), ↑(m - n) = m - n
Nat.cast_tsub
@[simp, norm_cast] theorem
cast_min: ∀ [inst : LinearOrderedSemiring α] {a b : }, ↑(min a b) = min a b
cast_min
[
LinearOrderedSemiring: Type ?u.23104 → Type ?u.23104
LinearOrderedSemiring
α: Type ?u.23098
α
] {
a:
a
b:
b
:
: Type
} : ((
min: {α : Type ?u.23114} → [self : Min α] → ααα
min
a:
a
b:
b
:
: Type
) :
α: Type ?u.23098
α
) =
min: {α : Type ?u.23206} → [self : Min α] → ααα
min
(
a:
a
:
α: Type ?u.23098
α
)
b:
b
:= (@
mono_cast: ∀ {α : Type ?u.23344} [inst : OrderedSemiring α], Monotone Nat.cast
mono_cast
α: Type ?u.23098
α
_).
map_min: ∀ {α : Type ?u.23402} {β : Type ?u.23401} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : αβ} {a b : α}, Monotone ff (min a b) = min (f a) (f b)
map_min
#align nat.cast_min
Nat.cast_min: ∀ {α : Type u_1} [inst : LinearOrderedSemiring α] {a b : }, ↑(min a b) = min a b
Nat.cast_min
@[simp, norm_cast] theorem
cast_max: ∀ {α : Type u_1} [inst : LinearOrderedSemiring α] {a b : }, ↑(max a b) = max a b
cast_max
[
LinearOrderedSemiring: Type ?u.23628 → Type ?u.23628
LinearOrderedSemiring
α: Type ?u.23622
α
] {
a:
a
b:
b
:
: Type
} : ((
max: {α : Type ?u.23638} → [self : Max α] → ααα
max
a:
a
b:
b
:
: Type
) :
α: Type ?u.23622
α
) =
max: {α : Type ?u.23730} → [self : Max α] → ααα
max
(
a:
a
:
α: Type ?u.23622
α
)
b:
b
:= (@
mono_cast: ∀ {α : Type ?u.23868} [inst : OrderedSemiring α], Monotone Nat.cast
mono_cast
α: Type ?u.23622
α
_).
map_max: ∀ {α : Type ?u.23926} {β : Type ?u.23925} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : αβ} {a b : α}, Monotone ff (max a b) = max (f a) (f b)
map_max
#align nat.cast_max
Nat.cast_max: ∀ {α : Type u_1} [inst : LinearOrderedSemiring α] {a b : }, ↑(max a b) = max a b
Nat.cast_max
@[simp, norm_cast] theorem
abs_cast: ∀ [inst : LinearOrderedRing α] (a : ), abs a = a
abs_cast
[
LinearOrderedRing: Type ?u.24152 → Type ?u.24152
LinearOrderedRing
α: Type ?u.24146
α
] (
a:
a
:
: Type
) : |(
a:
a
:
α: Type ?u.24146
α
)| =
a:
a
:=
abs_of_nonneg: ∀ {α : Type ?u.24423} [inst : AddGroup α] [inst_1 : LinearOrder α] [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α}, 0 aabs a = a
abs_of_nonneg
(
cast_nonneg: ∀ {α : Type ?u.24616} [inst : OrderedSemiring α] (n : ), 0 n
cast_nonneg
a:
a
) #align nat.abs_cast
Nat.abs_cast: ∀ {α : Type u_1} [inst : LinearOrderedRing α] (a : ), abs a = a
Nat.abs_cast
theorem
coe_nat_dvd: ∀ [inst : Semiring α] {m n : }, m nm n
coe_nat_dvd
[
Semiring: Type ?u.24846 → Type ?u.24846
Semiring
α: Type ?u.24840
α
] {
m:
m
n:
n
:
: Type
} (
h: m n
h
:
m:
m
n:
n
) : (
m:
m
:
α: Type ?u.24840
α
) ∣ (
n:
n
:
α: Type ?u.24840
α
) :=
map_dvd: ∀ {M : Type ?u.25078} {N : Type ?u.25079} [inst : Monoid M] [inst_1 : Monoid N] {F : Type ?u.25077} [inst_2 : MulHomClass F M N] (f : F) {a b : M}, a bf a f b
map_dvd
(
Nat.castRingHom: (α : Type ?u.25086) → [inst : NonAssocSemiring α] → →+* α
Nat.castRingHom
α: Type ?u.24840
α
)
h: m n
h
#align nat.coe_nat_dvd
Nat.coe_nat_dvd: ∀ {α : Type u_1} [inst : Semiring α] {m n : }, m nm n
Nat.coe_nat_dvd
alias
coe_nat_dvd: ∀ {α : Type u_1} [inst : Semiring α] {m n : }, m nm n
coe_nat_dvd
_root_.Dvd.dvd.natCast: ∀ {α : Type u_1} [inst : Semiring α] {m n : }, m nm n
_root_.Dvd.dvd.natCast
end Nat
instance: ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst : CharZero α], Nontrivial α
instance
[
AddMonoidWithOne: Type ?u.25690 → Type ?u.25690
AddMonoidWithOne
α: Type ?u.25684
α
] [
CharZero: (R : Type ?u.25693) → [inst : AddMonoidWithOne R] → Prop
CharZero
α: Type ?u.25684
α
] :
Nontrivial: Type ?u.25702 → Prop
Nontrivial
α: Type ?u.25684
α
where exists_pair_ne := ⟨
1: ?m.25722
1
,
0: ?m.25927
0
, (
Nat.cast_one: ∀ {R : Type ?u.26344} [inst : AddMonoidWithOne R], 1 = 1
Nat.cast_one
(R :=
α: Type ?u.25684
α
) ▸
Nat.cast_ne_zero: ∀ {R : Type ?u.26349} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {n : }, n 0 n 0
Nat.cast_ne_zero
.
2: ∀ {a b : Prop}, (a b) → ba
2
(

Goals accomplished! 🐙
α: Type ?u.25684

β: Type ?u.25687

inst✝¹: AddMonoidWithOne α

inst✝: CharZero α


1 0

Goals accomplished! 🐙
))⟩ section AddMonoidHomClass variable {
A: Type ?u.33337
A
B: Type ?u.26449
B
F: Type ?u.35455
F
:
Type _: Type (?u.35452+1)
Type _
} [
AddMonoidWithOne: Type ?u.35458 → Type ?u.35458
AddMonoidWithOne
B: Type ?u.26449
B
] theorem
ext_nat': ∀ {A : Type u_1} {F : Type u_2} [inst : AddMonoid A] [inst_1 : AddMonoidHomClass F A] (f g : F), f 1 = g 1f = g
ext_nat'
[
AddMonoid: Type ?u.26476 → Type ?u.26476
AddMonoid
A: Type ?u.26464
A
] [
AddMonoidHomClass: Type ?u.26481 → (M : outParam (Type ?u.26480)) → (N : outParam (Type ?u.26479)) → [inst : AddZeroClass M] → [inst : AddZeroClass N] → Type (max(max?u.26481?u.26480)?u.26479)
AddMonoidHomClass
F: Type ?u.26470
F
: Type
A: Type ?u.26464
A
] (
f: F
f
g: F
g
:
F: Type ?u.26470
F
) (
h: f 1 = g 1
h
:
f: F
f
1: ?m.27487
1
=
g: F
g
1: ?m.28454
1
) :
f: F
f
=
g: F
g
:=
FunLike.ext: ∀ {F : Sort ?u.28469} {α : Sort ?u.28470} {β : αSort ?u.28468} [i : FunLike F α β] (f g : F), (∀ (x : α), f x = g x) → f = g
FunLike.ext
f: F
f
g: F
g
<|

Goals accomplished! 🐙
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1


∀ (x : ), f x = g x
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1

n:


f n = g n
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1


∀ (x : ), f x = g x
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1

n:


f n = g n
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1


zero
f Nat.zero = g Nat.zero
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1


zero
f Nat.zero = g Nat.zero
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1


zero
f 0 = g 0
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1


zero
f Nat.zero = g Nat.zero
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1


zero
0 = g 0
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1


zero
f Nat.zero = g Nat.zero

Goals accomplished! 🐙

Goals accomplished! 🐙
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1

n:


f n = g n
α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F A

f, g: F

h: f 1 = g 1

n:

ihn: f n = g n


succ
f (Nat.succ n) = g (Nat.succ n)

Goals accomplished! 🐙
#align ext_nat'
ext_nat': ∀ {A : Type u_1} {F : Type u_2} [inst : AddMonoid A] [inst_1 : AddMonoidHomClass F A] (f g : F), f 1 = g 1f = g
ext_nat'
@[ext] theorem
AddMonoidHom.ext_nat: ∀ [inst : AddMonoid A] {f g : →+ A}, f 1 = g 1f = g
AddMonoidHom.ext_nat
[
AddMonoid: Type ?u.33349 → Type ?u.33349
AddMonoid
A: Type ?u.33337
A
] {
f: →+ A
f
g: →+ A
g
:
: Type
→+
A: Type ?u.33337
A
} :
f: →+ A
f
1: ?m.34371
1
=
g: →+ A
g
1: ?m.35344
1
f: →+ A
f
=
g: →+ A
g
:=
ext_nat': ∀ {A : Type ?u.35355} {F : Type ?u.35356} [inst : AddMonoid A] [inst_1 : AddMonoidHomClass F A] (f g : F), f 1 = g 1f = g
ext_nat'
f: →+ A
f
g: →+ A
g
#align add_monoid_hom.ext_nat
AddMonoidHom.ext_nat: ∀ {A : Type u_1} [inst : AddMonoid A] {f g : →+ A}, f 1 = g 1f = g
AddMonoidHom.ext_nat
variable [
AddMonoidWithOne: Type ?u.40894 → Type ?u.40894
AddMonoidWithOne
A: Type ?u.35470
A
] -- these versions are primed so that the `RingHomClass` versions aren't theorem
eq_natCast': ∀ [inst : AddMonoidHomClass F A] (f : F), f 1 = 1∀ (n : ), f n = n
eq_natCast'
[
AddMonoidHomClass: Type ?u.35487 → (M : outParam (Type ?u.35486)) → (N : outParam (Type ?u.35485)) → [inst : AddZeroClass M] → [inst : AddZeroClass N] → Type (max(max?u.35487?u.35486)?u.35485)
AddMonoidHomClass
F: Type ?u.35476
F
: Type
A: Type ?u.35470
A
] (
f: F
f
:
F: Type ?u.35476
F
) (
h1: f 1 = 1
h1
:
f: F
f
1: ?m.36497
1
=
1: ?m.36508
1
) : ∀
n:
n
:
: Type
,
f: F
f
n:
n
=
n:
n
|
0:
0
=>

Goals accomplished! 🐙
α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A

f: F

h1: f 1 = 1


f 0 = 0

Goals accomplished! 🐙
|
n:
n
+ 1 =>

Goals accomplished! 🐙
α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A

f: F

h1: f 1 = 1

n:


f (n + 1) = ↑(n + 1)
α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A

f: F

h1: f 1 = 1

n:


f (n + 1) = ↑(n + 1)
α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A

f: F

h1: f 1 = 1

n:


f n + f 1 = ↑(n + 1)
α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A

f: F

h1: f 1 = 1

n:


f (n + 1) = ↑(n + 1)
α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A

f: F

h1: f 1 = 1

n:


f n + 1 = ↑(n + 1)
α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A

f: F

h1: f 1 = 1

n:


f (n + 1) = ↑(n + 1)
α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A

f: F

h1: f 1 = 1

n:


n + 1 = ↑(n + 1)
α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A

f: F

h1: f 1 = 1

n:


f (n + 1) = ↑(n + 1)
α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A

f: F

h1: f 1 = 1

n:


n + 1 = n + 1

Goals accomplished! 🐙
#align eq_nat_cast'
eq_natCast': ∀ {A : Type u_2} {F : Type u_1} [inst : AddMonoidWithOne A] [inst_1 : AddMonoidHomClass F A] (f : F), f 1 = 1∀ (n : ), f n = n
eq_natCast'
theorem
map_natCast': ∀ {B : Type u_3} {F : Type u_2} [inst : AddMonoidWithOne B] {A : Type u_1} [inst_1 : AddMonoidWithOne A] [inst_2 : AddMonoidHomClass F A B] (f : F), f 1 = 1∀ (n : ), f n = n
map_natCast'
{
A: Type u_1
A
} [
AddMonoidWithOne: Type ?u.40900 → Type ?u.40900
AddMonoidWithOne
A: ?m.40897
A
] [
AddMonoidHomClass: Type ?u.40905 → (M : outParam (Type ?u.40904)) → (N : outParam (Type ?u.40903)) → [inst : AddZeroClass M] → [inst : AddZeroClass N] → Type (max(max?u.40905?u.40904)?u.40903)
AddMonoidHomClass
F: Type ?u.40888
F
A: ?m.40897
A
B: Type ?u.40885
B
] (
f: F
f
:
F: Type ?u.40888
F
) (
h: f 1 = 1
h
:
f: F
f
1: ?m.41921
1
=
1: ?m.42117
1
) : ∀
n:
n
:
: Type
,
f: F
f
n:
n
=
n:
n
|
0:
0
=>

Goals accomplished! 🐙
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1


f 0 = 0

Goals accomplished! 🐙
|
n:
n
+ 1 =>

Goals accomplished! 🐙
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


f ↑(n + 1) = ↑(n + 1)
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


f ↑(n + 1) = ↑(n + 1)
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


f (n + 1) = ↑(n + 1)
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


f ↑(n + 1) = ↑(n + 1)
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


f n + f 1 = ↑(n + 1)
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


f ↑(n + 1) = ↑(n + 1)
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


f n + f 1 = n + 1
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


f ↑(n + 1) = ↑(n + 1)
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


n + f 1 = n + 1
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


f ↑(n + 1) = ↑(n + 1)
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


n + f 1 = n + 1
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


f ↑(n + 1) = ↑(n + 1)
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


n + 1 = n + 1
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


f ↑(n + 1) = ↑(n + 1)
α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: f 1 = 1

n:


n + 1 = n + 1

Goals accomplished! 🐙
#align map_nat_cast'
map_natCast': ∀ {B : Type u_3} {F : Type u_2} [inst : AddMonoidWithOne B] {A : Type u_1} [inst_1 : AddMonoidWithOne A] [inst_2 : AddMonoidHomClass F A B] (f : F), f 1 = 1∀ (n : ), f n = n
map_natCast'
end AddMonoidHomClass section MonoidWithZeroHomClass variable {
A: Type ?u.48254
A
F: Type ?u.48257
F
:
Type _: Type (?u.48242+1)
Type _
} [
MulZeroOneClass: Type ?u.48245 → Type ?u.48245
MulZeroOneClass
A: Type ?u.48239
A
] /-- If two `MonoidWithZeroHom`s agree on the positive naturals they are equal. -/ theorem
ext_nat'': ∀ [inst : MonoidWithZeroHomClass F A] (f g : F), (∀ {n : }, 0 < nf n = g n) → f = g
ext_nat''
[
MonoidWithZeroHomClass: Type ?u.48265 → (M : outParam (Type ?u.48264)) → (N : outParam (Type ?u.48263)) → [inst : MulZeroOneClass M] → [inst : MulZeroOneClass N] → Type (max(max?u.48265?u.48264)?u.48263)
MonoidWithZeroHomClass
F: Type ?u.48257
F
: Type
A: Type ?u.48254
A
] (
f: F
f
g: F
g
:
F: Type ?u.48257
F
) (
h_pos: ∀ {n : }, 0 < nf n = g n
h_pos
: ∀ {
n:
n
:
: Type
},
0: ?m.48305
0
<
n:
n
f: F
f
n:
n
=
g: F
g
n:
n
) :
f: F
f
=
g: F
g
:=

Goals accomplished! 🐙
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n


f = g
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n


h
∀ (x : ), f x = g x
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n


f = g
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n


h.zero
f Nat.zero = g Nat.zero
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n

n:


h.succ
f (Nat.succ n) = g (Nat.succ n)
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n


f = g
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n


h.zero
f Nat.zero = g Nat.zero
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n


h.zero
f Nat.zero = g Nat.zero
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n

n:


h.succ
f (Nat.succ n) = g (Nat.succ n)

Goals accomplished! 🐙
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n


f = g
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n

n:


h.succ
f (Nat.succ n) = g (Nat.succ n)
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F A

f, g: F

h_pos: ∀ {n : }, 0 < nf n = g n

n:


h.succ
f (Nat.succ n) = g (Nat.succ n)

Goals accomplished! 🐙
#align ext_nat''
ext_nat'': ∀ {A : Type u_2} {F : Type u_1} [inst : MulZeroOneClass A] [inst_1 : MonoidWithZeroHomClass F A] (f g : F), (∀ {n : }, 0 < nf n = g n) → f = g
ext_nat''
@[ext] theorem
MonoidWithZeroHom.ext_nat: ∀ {f g : →*₀ A}, (∀ {n : }, 0 < nf n = g n) → f = g
MonoidWithZeroHom.ext_nat
{f g :
: Type
→*₀
A: Type ?u.51912
A
} : (∀ {
n:
n
:
: Type
},
0: ?m.51965
0
<
n:
n
f
n:
n
= g
n:
n
) → f = g :=
ext_nat'': ∀ {A : Type ?u.53467} {F : Type ?u.53466} [inst : MulZeroOneClass A] [inst_1 : MonoidWithZeroHomClass F A] (f g : F), (∀ {n : }, 0 < nf n = g n) → f = g
ext_nat''
f g #align monoid_with_zero_hom.ext_nat
MonoidWithZeroHom.ext_nat: ∀ {A : Type u_1} [inst : MulZeroOneClass A] {f g : →*₀ A}, (∀ {n : }, 0 < nf n = g n) → f = g
MonoidWithZeroHom.ext_nat
end MonoidWithZeroHomClass section RingHomClass variable {
R: Type ?u.53572
R
S: Type ?u.53575
S
F: Type ?u.57182
F
:
Type _: Type (?u.57179+1)
Type _
} [
NonAssocSemiring: Type ?u.59361 → Type ?u.59361
NonAssocSemiring
R: Type ?u.53572
R
] [
NonAssocSemiring: Type ?u.55176 → Type ?u.55176
NonAssocSemiring
S: Type ?u.53554
S
] @[simp] theorem
eq_natCast: ∀ {R : Type u_2} {F : Type u_1} [inst : NonAssocSemiring R] [inst_1 : RingHomClass F R] (f : F) (n : ), f n = n
eq_natCast
[
RingHomClass: Type ?u.53589 → (α : outParam (Type ?u.53588)) → (β : outParam (Type ?u.53587)) → [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.53589?u.53588)?u.53587)
RingHomClass
F: Type ?u.53578
F
: Type
R: Type ?u.53572
R
] (
f: F
f
:
F: Type ?u.53578
F
) : ∀
n: ?m.53616
n
,
f: F
f
n: ?m.53616
n
=
n: ?m.53616
n
:=
eq_natCast': ∀ {A : Type ?u.54584} {F : Type ?u.54583} [inst : AddMonoidWithOne A] [inst_1 : AddMonoidHomClass F A] (f : F), f 1 = 1∀ (n : ), f n = n
eq_natCast'
f: F
f
<|
map_one: ∀ {M : Type ?u.54761} {N : Type ?u.54762} {F : Type ?u.54760} [inst : One M] [inst_1 : One N] [inst_2 : OneHomClass F M N] (f : F), f 1 = 1
map_one
f: F
f
#align eq_nat_cast
eq_natCast: ∀ {R : Type u_2} {F : Type u_1} [inst : NonAssocSemiring R] [inst_1 : RingHomClass F R] (f : F) (n : ), f n = n
eq_natCast
@[simp] theorem
map_natCast: ∀ {R : Type u_2} {S : Type u_3} {F : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] [inst_2 : RingHomClass F R S] (f : F) (n : ), f n = n
map_natCast
[
RingHomClass: Type ?u.55181 → (α : outParam (Type ?u.55180)) → (β : outParam (Type ?u.55179)) → [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.55181?u.55180)?u.55179)
RingHomClass
F: Type ?u.55170
F
R: Type ?u.55164
R
S: Type ?u.55167
S
] (
f: F
f
:
F: Type ?u.55170
F
) : ∀
n:
n
:
: Type
,
f: F
f
(
n:
n
:
R: Type ?u.55164
R
) =
n:
n
:=
map_natCast': ∀ {B : Type ?u.56359} {F : Type ?u.56358} [inst : AddMonoidWithOne B] {A : Type ?u.56357} [inst_1 : AddMonoidWithOne A] [inst_2 : AddMonoidHomClass F A B] (f : F), f 1 = 1∀ (n : ), f n = n
map_natCast'
f: F
f
<|
map_one: ∀ {M : Type ?u.56634} {N : Type ?u.56635} {F : Type ?u.56633} [inst : One M] [inst_1 : One N] [inst_2 : OneHomClass F M N] (f : F), f 1 = 1
map_one
f: F
f
#align map_nat_cast
map_natCast: ∀ {R : Type u_2} {S : Type u_3} {F : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] [inst_2 : RingHomClass F R S] (f : F) (n : ), f n = n
map_natCast
--Porting note: new theorem @[simp] theorem
map_ofNat: ∀ {R : Type u_2} {S : Type u_3} {F : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] [inst_2 : RingHomClass F R S] (f : F) (n : ) [inst_3 : Nat.AtLeastTwo n], f (OfNat.ofNat n) = OfNat.ofNat n
map_ofNat
[
RingHomClass: Type ?u.57193 → (α : outParam (Type ?u.57192)) → (β : outParam (Type ?u.57191)) → [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.57193?u.57192)?u.57191)
RingHomClass
F: Type ?u.57182
F
R: Type ?u.57176
R
S: Type ?u.57179
S
] (
f: F
f
:
F: Type ?u.57182
F
) (
n:
n
:
: Type
) [
Nat.AtLeastTwo: Prop
Nat.AtLeastTwo
n:
n
] : (
f: F
f
(
OfNat.ofNat: {α : Type ?u.57735} → (x : ) → [self : OfNat α x] → α
OfNat.ofNat
n:
n
) :
S: Type ?u.57179
S
) =
OfNat.ofNat: {α : Type ?u.57908} → (x : ) → [self : OfNat α x] → α
OfNat.ofNat
n:
n
:=
map_natCast: ∀ {R : Type ?u.58143} {S : Type ?u.58144} {F : Type ?u.58142} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] [inst_2 : RingHomClass F R S] (f : F) (n : ), f n = n
map_natCast
f: F
f
n:
n
theorem
ext_nat: ∀ [inst : RingHomClass F R] (f g : F), f = g
ext_nat
[
RingHomClass: Type ?u.58259 → (α : outParam (Type ?u.58258)) → (β : outParam (Type ?u.58257)) → [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.58259?u.58258)?u.58257)
RingHomClass
F: Type ?u.58248
F
: Type
R: Type ?u.58242
R
] (
f: F
f
g: F
g
:
F: Type ?u.58248
F
) :
f: F
f
=
g: F
g
:=
ext_nat': ∀ {A : Type ?u.58293} {F : Type ?u.58294} [inst : AddMonoid A] [inst_1 : AddMonoidHomClass F A] (f g : F), f 1 = g 1f = g
ext_nat'
f: F
f
g: F
g
<|

Goals accomplished! 🐙
α: Type ?u.58236

β: Type ?u.58239

R: Type u_2

S: Type ?u.58245

F: Type u_1

inst✝²: NonAssocSemiring R

inst✝¹: NonAssocSemiring S

inst✝: RingHomClass F R

f, g: F


f 1 = g 1

Goals accomplished! 🐙
#align ext_nat
ext_nat: ∀ {R : Type u_2} {F : Type u_1} [inst : NonAssocSemiring R] [inst : RingHomClass F R] (f g : F), f = g
ext_nat
theorem
NeZero.nat_of_injective: ∀ {n : } [h : NeZero n] [inst : RingHomClass F R S] {f : F}, Function.Injective fNeZero n
NeZero.nat_of_injective
{
n:
n
:
: Type
} [
h: NeZero n
h
:
NeZero: {R : Type ?u.59369} → [inst : Zero R] → RProp
NeZero
(
n:
n
:
R: Type ?u.59352
R
)] [
RingHomClass: Type ?u.59786 → (α : outParam (Type ?u.59785)) → (β : outParam (Type ?u.59784)) → [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.59786?u.59785)?u.59784)
RingHomClass
F: Type ?u.59358
F
R: Type ?u.59352
R
S: Type ?u.59355
S
] {
f: F
f
:
F: Type ?u.59358
F
} (hf :
Function.Injective: {α : Sort ?u.59802} → {β : Sort ?u.59801} → (αβ) → Prop
Function.Injective
f: F
f
) :
NeZero: {R : Type ?u.60327} → [inst : Zero R] → RProp
NeZero
(
n:
n
:
S: Type ?u.59355
S
) := ⟨fun
h: ?m.60790
h
NeZero.natCast_ne: ∀ (n : ) (R : Type ?u.60792) [inst : AddMonoidWithOne R] [h : NeZero n], n 0
NeZero.natCast_ne
n:
n
R: Type ?u.59352
R
<| hf <|

Goals accomplished! 🐙
α: Type ?u.59346

β: Type ?u.59349

R: Type u_1

S: Type u_3

F: Type u_2

inst✝²: NonAssocSemiring R

inst✝¹: NonAssocSemiring S

n:

h✝: NeZero n

inst✝: RingHomClass F R S

f: F

hf: Function.Injective f

h: n = 0


f n = f 0

Goals accomplished! 🐙
#align ne_zero.nat_of_injective
NeZero.nat_of_injective: ∀ {R : Type u_1} {S : Type u_3} {F : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {n : } [h : NeZero n] [inst_2 : RingHomClass F R S] {f : F}, Function.Injective fNeZero n
NeZero.nat_of_injective
theorem
NeZero.nat_of_neZero: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {F : Type u_3} [inst_2 : RingHomClass F R S], F∀ {n : } [hn : NeZero n], NeZero n
NeZero.nat_of_neZero
{
R: Type u_1
R
S: ?m.61830
S
} [
Semiring: Type ?u.61833 → Type ?u.61833
Semiring
R: ?m.61827
R
] [
Semiring: Type ?u.61836 → Type ?u.61836
Semiring
S: ?m.61830
S
] {
F: ?m.61839
F
} [
RingHomClass: Type ?u.61844 → (α : outParam (Type ?u.61843)) → (β : outParam (Type ?u.61842)) → [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.61844?u.61843)?u.61842)
RingHomClass
F: ?m.61839
F
R: ?m.61827
R
S: ?m.61830
S
] (
f: F
f
:
F: ?m.61839
F
) {
n:
n
:
: Type
} [
hn: NeZero n
hn
:
NeZero: {R : Type ?u.61881} → [inst : Zero R] → RProp
NeZero
(
n:
n
:
S: ?m.61830
S
)] :
NeZero: {R : Type ?u.62079} → [inst : Zero R] → RProp
NeZero
(
n:
n
:
R: ?m.61827
R
) :=
.of_map: ∀ {F : Type ?u.62287} {R : Type ?u.62285} {M : Type ?u.62286} [inst : Zero R] [inst_1 : Zero M] [inst_2 : ZeroHomClass F R M] (f : F) {r : R} [neZero : NeZero (f r)], NeZero r
.of_map
(f :=
f: F
f
) (neZero :=

Goals accomplished! 🐙
α: Type ?u.61806

β: Type ?u.61809

R✝: Type ?u.61812

S✝: Type ?u.61815

F✝: Type ?u.61818

inst✝⁴: NonAssocSemiring R✝

inst✝³: NonAssocSemiring S✝

R: Type u_1

S: Type u_2

inst✝²: Semiring R

inst✝¹: Semiring S

F: Type u_3

inst✝: RingHomClass F R S

f: F

n:

hn: NeZero n


NeZero (f n)

Goals accomplished! 🐙
) #align ne_zero.nat_of_ne_zero
NeZero.nat_of_neZero: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {F : Type u_3} [inst_2 : RingHomClass F R S], F∀ {n : } [hn : NeZero n], NeZero n
NeZero.nat_of_neZero
end RingHomClass namespace RingHom /-- This is primed to match `eq_intCast'`. -/ theorem
eq_natCast': ∀ {R : Type u_1} [inst : NonAssocSemiring R] (f : →+* R), f = Nat.castRingHom R
eq_natCast'
{
R: ?m.62990
R
} [
NonAssocSemiring: Type ?u.62993 → Type ?u.62993
NonAssocSemiring
R: ?m.62990
R
] (
f: →+* R
f
:
: Type
→+*
R: ?m.62990
R
) :
f: →+* R
f
=
Nat.castRingHom: (α : Type ?u.63021) → [inst : NonAssocSemiring α] → →+* α
Nat.castRingHom
R: ?m.62990
R
:=
RingHom.ext: ∀ {α : Type ?u.63032} {β : Type ?u.63033} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄, (∀ (x_2 : α), f x_2 = g x_2) → f = g
RingHom.ext
<|
eq_natCast: ∀ {R : Type ?u.63049} {F : Type ?u.63048} [inst : NonAssocSemiring R] [inst_1 : RingHomClass F R] (f : F) (n : ), f n = n
eq_natCast
f: →+* R
f
#align ring_hom.eq_nat_cast'
RingHom.eq_natCast': ∀ {R : Type u_1} [inst : NonAssocSemiring R] (f : →+* R), f = Nat.castRingHom R
RingHom.eq_natCast'
end RingHom @[simp, norm_cast] theorem
Nat.cast_id: ∀ (n : ), n = n
Nat.cast_id
(
n:
n
:
: Type
) :
n:
n
.
cast: {R : Type ?u.63109} → [inst : NatCast R] → R
cast
=
n:
n
:=
rfl: ∀ {α : Sort ?u.63154} {a : α}, a = a
rfl
#align nat.cast_id
Nat.cast_id: ∀ (n : ), n = n
Nat.cast_id
@[simp] theorem
Nat.castRingHom_nat: castRingHom = RingHom.id
Nat.castRingHom_nat
:
Nat.castRingHom: (α : Type ?u.63190) → [inst : NonAssocSemiring α] → →+* α
Nat.castRingHom
: Type
=
RingHom.id: (α : Type ?u.63206) → [inst : NonAssocSemiring α] → α →+* α
RingHom.id
: Type
:=
rfl: ∀ {α : Sort ?u.63214} {a : α}, a = a
rfl
#align nat.cast_ring_hom_nat
Nat.castRingHom_nat: Nat.castRingHom = RingHom.id
Nat.castRingHom_nat
/-- We don't use `RingHomClass` here, since that might cause type-class slowdown for `Subsingleton`-/ instance
Nat.uniqueRingHom: {R : Type u_1} → [inst : NonAssocSemiring R] → Unique ( →+* R)
Nat.uniqueRingHom
{
R: Type ?u.63256
R
:
Type _: Type (?u.63256+1)
Type _
} [
NonAssocSemiring: Type ?u.63259 → Type ?u.63259
NonAssocSemiring
R: Type ?u.63256
R
] :
Unique: Sort ?u.63262 → Sort (max1?u.63262)
Unique
(
: Type
→+*
R: Type ?u.63256
R
) where default :=
Nat.castRingHom: (α : Type ?u.63295) → [inst : NonAssocSemiring α] → →+* α
Nat.castRingHom
R: Type ?u.63256
R
uniq :=
RingHom.eq_natCast': ∀ {R : Type ?u.63304} [inst : NonAssocSemiring R] (f : →+* R), f = castRingHom R
RingHom.eq_natCast'
namespace Pi variable {
π: αType ?u.64938
π
:
α: Type ?u.63375
α
Type _: Type (?u.63364+1)
Type _
} [∀
a: ?m.63368
a
,
NatCast: Type ?u.63371 → Type ?u.63371
NatCast
(
π: αType ?u.63364
π
a: ?m.63368
a
)] /- Porting note: manually wrote this instance. Was `by refine_struct { .. } <;> pi_instance_derive_field` -/ instance
natCast: NatCast ((a : α) → π a)
natCast
:
NatCast: Type ?u.63394 → Type ?u.63394
NatCast
(∀
a: ?m.63396
a
,
π: αType ?u.63383
π
a: ?m.63396
a
) := { natCast := fun
n: ?m.63407
n
_: ?m.63410
_
n: ?m.63407
n
} theorem
nat_apply: ∀ {α : Type u_2} {π : αType u_1} [inst : (a : α) → NatCast (π a)] (n : ) (a : α), n a = n
nat_apply
(
n:
n
:
: Type
) (
a: α
a
:
α: Type ?u.63536
α
) : (
n:
n
: ∀
a: ?m.63562
a
,
π: αType ?u.63544
π
a: ?m.63562
a
)
a: α
a
=
n:
n
:=
rfl: ∀ {α : Sort ?u.64910} {a : α}, a = a
rfl
#align pi.nat_apply
Pi.nat_apply: ∀ {α : Type u_2} {π : αType u_1} [inst : (a : α) → NatCast (π a)] (n : ) (a : α), n a = n
Pi.nat_apply
@[simp] theorem
coe_nat: ∀ {α : Type u_1} {π : αType u_2} [inst : (a : α) → NatCast (π a)] (n : ), n = fun x => n
coe_nat
(
n:
n
:
: Type
) : (
n:
n
: ∀
a: ?m.64954
a
,
π: αType ?u.64938
π
a: ?m.64954
a
) = fun
_: ?m.66225
_
↦ ↑
n:
n
:=
rfl: ∀ {α : Sort ?u.66316} {a : α}, a = a
rfl
#align pi.coe_nat
Pi.coe_nat: ∀ {α : Type u_1} {π : αType u_2} [inst : (a : α) → NatCast (π a)] (n : ), n = fun x => n
Pi.coe_nat
end Pi theorem
Sum.elim_natCast_natCast: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : NatCast γ] (n : ), Sum.elim n n = n
Sum.elim_natCast_natCast
{
α: Type ?u.66355
α
β: Type ?u.66358
β
γ: Type ?u.66361
γ
:
Type _: Type (?u.66355+1)
Type _
} [
NatCast: Type ?u.66364 → Type ?u.66364
NatCast
γ: Type ?u.66361
γ
] (
n:
n
:
: Type
) :
Sum.elim: {α : Type ?u.66372} → {β : Type ?u.66371} → {γ : Sort ?u.66370} → (αγ) → (βγ) → α βγ
Sum.elim
(
n:
n
:
α: Type ?u.66355
α
γ: Type ?u.66361
γ
) (
n:
n
:
β: Type ?u.66358
β
γ: Type ?u.66361
γ
) =
n:
n
:= @
Sum.elim_lam_const_lam_const: ∀ {α : Type ?u.70246} {β : Type ?u.70245} {γ : Type ?u.70247} (c : γ), (Sum.elim (fun x => c) fun x => c) = fun x => c
Sum.elim_lam_const_lam_const
α: Type u_1
α
β: Type u_2
β
γ: Type u_3
γ
n:
n
#align sum.elim_nat_cast_nat_cast
Sum.elim_natCast_natCast: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : NatCast γ] (n : ), Sum.elim n n = n
Sum.elim_natCast_natCast
/-! ### Order dual -/ open OrderDual
instance: {α : Type u_1} → [h : NatCast α] → NatCast αᵒᵈ
instance
[
h: NatCast α
h
:
NatCast: Type ?u.70320 → Type ?u.70320
NatCast
α: Type ?u.70314
α
] :
NatCast: Type ?u.70323 → Type ?u.70323
NatCast
α: Type ?u.70314
α
ᵒᵈ :=
h: NatCast α
h
instance: {α : Type u_1} → [h : AddMonoidWithOne α] → AddMonoidWithOne αᵒᵈ
instance
[h :
AddMonoidWithOne: Type ?u.70364 → Type ?u.70364
AddMonoidWithOne
α: Type ?u.70358
α
] :
AddMonoidWithOne: Type ?u.70367 → Type ?u.70367
AddMonoidWithOne
α: Type ?u.70358
α
ᵒᵈ := h
instance: {α : Type u_1} → [h : AddCommMonoidWithOne α] → AddCommMonoidWithOne αᵒᵈ
instance
[h :
AddCommMonoidWithOne: Type ?u.70408 → Type ?u.70408
AddCommMonoidWithOne
α: Type ?u.70402
α
] :
AddCommMonoidWithOne: Type ?u.70411 → Type ?u.70411
AddCommMonoidWithOne
α: Type ?u.70402
α
ᵒᵈ := h @[simp] theorem
toDual_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ), toDual n = n
toDual_natCast
[
NatCast: Type ?u.70452 → Type ?u.70452
NatCast
α: Type ?u.70446
α
] (
n:
n
:
: Type
) :
toDual: {α : Type ?u.70458} → α αᵒᵈ
toDual
(
n:
n
:
α: Type ?u.70446
α
) =
n:
n
:=
rfl: ∀ {α : Sort ?u.70683} {a : α}, a = a
rfl
#align to_dual_nat_cast
toDual_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ), toDual n = n
toDual_natCast
@[simp] theorem
ofDual_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ), ↑(ofDual n) = n
ofDual_natCast
[
NatCast: Type ?u.70725 → Type ?u.70725
NatCast
α: Type ?u.70719
α
] (
n:
n
:
: Type
) : (
ofDual: {α : Type ?u.70732} → αᵒᵈ α
ofDual
n:
n
:
α: Type ?u.70719
α
) =
n:
n
:=
rfl: ∀ {α : Sort ?u.70933} {a : α}, a = a
rfl
#align of_dual_nat_cast
ofDual_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ), ↑(ofDual n) = n
ofDual_natCast
/-! ### Lexicographic order -/
instance: {α : Type u_1} → [h : NatCast α] → NatCast (Lex α)
instance
[
h: NatCast α
h
:
NatCast: Type ?u.70975 → Type ?u.70975
NatCast
α: Type ?u.70969
α
] :
NatCast: Type ?u.70978 → Type ?u.70978
NatCast
(
Lex: Type ?u.70979 → Type ?u.70979
Lex
α: Type ?u.70969
α
) :=
h: NatCast α
h
instance: {α : Type u_1} → [h : AddMonoidWithOne α] → AddMonoidWithOne (Lex α)
instance
[h :
AddMonoidWithOne: Type ?u.71019 → Type ?u.71019
AddMonoidWithOne
α: Type ?u.71013
α
] :
AddMonoidWithOne: Type ?u.71022 → Type ?u.71022
AddMonoidWithOne
(
Lex: Type ?u.71023 → Type ?u.71023
Lex
α: Type ?u.71013
α
) := h
instance: {α : Type u_1} → [h : AddCommMonoidWithOne α] → AddCommMonoidWithOne (Lex α)
instance
[h :
AddCommMonoidWithOne: Type ?u.71063 → Type ?u.71063
AddCommMonoidWithOne
α: Type ?u.71057
α
] :
AddCommMonoidWithOne: Type ?u.71066 → Type ?u.71066
AddCommMonoidWithOne
(
Lex: Type ?u.71067 → Type ?u.71067
Lex
α: Type ?u.71057
α
) := h @[simp] theorem
toLex_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ), toLex n = n
toLex_natCast
[
NatCast: Type ?u.71107 → Type ?u.71107
NatCast
α: Type ?u.71101
α
] (
n:
n
:
: Type
) :
toLex: {α : Type ?u.71113} → α Lex α
toLex
(
n:
n
:
α: Type ?u.71101
α
) =
n:
n
:=
rfl: ∀ {α : Sort ?u.71338} {a : α}, a = a
rfl
#align to_lex_nat_cast
toLex_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ), toLex n = n
toLex_natCast
@[simp] theorem
ofLex_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ), ↑(ofLex n) = n
ofLex_natCast
[
NatCast: Type ?u.71380 → Type ?u.71380
NatCast
α: Type ?u.71374
α
] (
n:
n
:
: Type
) : (
ofLex: {α : Type ?u.71387} → Lex α α
ofLex
n:
n
:
α: Type ?u.71374
α
) =
n:
n
:=
rfl: ∀ {α : Sort ?u.71588} {a : α}, a = a
rfl
#align of_lex_nat_cast
ofLex_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ), ↑(ofLex n) = n
ofLex_natCast