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
Cmd instead of
Ctrl .
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
Ported by: Scott Morrison
! This file was ported from Lean 3 source module data.int.cast.lemmas
! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Int.Order.Basic
import Mathlib.Data.Nat.Cast.Basic
/-!
# Cast of integers (additional theorems)
This file proves additional properties about the *canonical* homomorphism from
the integers into an additive group with a one (`Int.cast`),
particularly results involving algebraic homomorphisms or the order structure on `ℤ`
which were not available in the import dependencies of `Data.Int.Cast.Basic`.
## Main declarations
* `castAddHom`: `cast` bundled as an `AddMonoidHom`.
* `castRingHom`: `cast` bundled as a `RingHom`.
-/
open Nat
variable { F ι α β : Type _ : Type (?u.68416+1)}
namespace Int
/-- Coercion `ℕ → ℤ` as a `RingHom`. -/
def ofNatHom : ℕ →+* ℤ :=
Nat.castRingHom ℤ
#align int.of_nat_hom Int.ofNatHom
-- Porting note: no need to be `@[simp]`, as `Nat.cast_pos` handles this.
-- @[simp]
theorem coe_nat_pos : ∀ {n : ℕ }, 0 < ↑n ↔ 0 < n coe_nat_pos { n : ℕ } : ( 0 : ℤ ) < n ↔ 0 < n :=
Nat.cast_pos
#align int.coe_nat_pos Int.coe_nat_pos : ∀ {n : ℕ }, 0 < ↑n ↔ 0 < n
theorem coe_nat_succ_pos ( n : ℕ ) : 0 < ( n . succ : ℤ ) :=
Int.coe_nat_pos : ∀ {n : ℕ }, 0 < ↑n ↔ 0 < n . 2 : ∀ {a b : Prop }, (a ↔ b b → a ( succ_pos n )
#align int.coe_nat_succ_pos Int.coe_nat_succ_pos : ∀ (n : ℕ ), 0 < ↑(Nat.succ n
lemma toNat_lt' : ∀ {a : ℤ } {b : ℕ }, b ≠ 0 toNat a < b ↔ a < ↑b toNat_lt' { a : ℤ } { b : ℕ } ( hb : b ≠ 0 ) : a . toNat < b ↔ a < b := by
rw [ ← toNat_lt_toNat , toNat_coe_nat : ∀ (n : ℕ ), toNat ↑n = n ] ; exact coe_nat_pos : ∀ {n : ℕ }, 0 < ↑n ↔ 0 < n . 2 : ∀ {a b : Prop }, (a ↔ b b → a hb . bot_lt
#align int.to_nat_lt Int.toNat_lt' : ∀ {a : ℤ } {b : ℕ }, b ≠ 0 toNat a < b ↔ a < ↑b
lemma natMod_lt : ∀ {a : ℤ } {b : ℕ }, b ≠ 0 natMod a ↑b < b natMod_lt { a : ℤ } { b : ℕ } ( hb : b ≠ 0 ) : a . natMod b < b :=
( toNat_lt' : ∀ {a : ℤ } {b : ℕ }, b ≠ 0 toNat a < b ↔ a < ↑b hb ). 2 : ∀ {a b : Prop }, (a ↔ b b → a $ emod_lt_of_pos : ∀ (a : ℤ ) {b : ℤ }, 0 < b a % b < b _ $ coe_nat_pos : ∀ {n : ℕ }, 0 < ↑n ↔ 0 < n . 2 : ∀ {a b : Prop }, (a ↔ b b → a hb . bot_lt
#align int.nat_mod_lt Int.natMod_lt : ∀ {a : ℤ } {b : ℕ }, b ≠ 0 natMod a ↑b < b
section cast
@[ simp , norm_cast ]
theorem cast_mul [ NonAssocRing : Type ?u.1336 → Type ?u.1336 α ] : ∀ m n , (( m * n : ℤ ) : α ) = m * n := fun m =>
Int.inductionOn' : ∀ {C : ℤ → Sort ?u.1849z b : ℤ ),
C b (∀ (k : ℤ ), b ≤ k C k C (k + 1 ) → (∀ (k : ℤ ), k ≤ b C k C (k - 1 ) → C z m 0 ( by ∀ (n : ℤ ), ↑(0 * n = ↑0 * ↑n simp ) ( fun k _ ih n => by ↑((k + 1 * n ) = ↑(k + 1 * ↑n simp [ add_mul , ih : ∀ (n : ℤ ), ↑(k * n = ↑k * ↑n ih ] ) fun k _ ih n => by
↑((k - 1 * n ) = ↑(k - 1 * ↑n simp [ sub_mul , ih : ∀ (n : ℤ ), ↑(k * n = ↑k * ↑n ih ]
#align int.cast_mul Int.cast_mulₓ -- dubious translation, type involves HasLiftT
@[ simp , norm_cast ]
theorem cast_ite [ AddGroupWithOne : Type ?u.3569 → Type ?u.3569 α ] ( P : Prop ) [ Decidable P ] ( m n : ℤ ) :
(( ite P m n : ℤ ) : α ) = ite P ( m : α ) ( n : α ) :=
apply_ite : ∀ {α : Sort ?u.3881} {β : Sort ?u.3882} (f : α → β P : Prop ) [inst : Decidable P x y : α ),
f (if P then x else y )= if P then f x f y _ _ _ _
#align int.cast_ite Int.cast_ite
/-- `coe : ℤ → α` as an `AddMonoidHom`. -/
def castAddHom ( α : Type _ ) [ AddGroupWithOne : Type ?u.4182 → Type ?u.4182 α ] : ℤ →+ α where
toFun := Int.cast
map_zero' := cast_zero
map_add' := cast_add
#align int.cast_add_hom Int.castAddHom
@[ simp ]
theorem coe_castAddHom [ AddGroupWithOne : Type ?u.4896 → Type ?u.4896 α ] : ⇑( castAddHom α ) = fun x : ℤ => ( x : α ) :=
rfl : ∀ {α : Sort ?u.5811} {a : α }, a = a
#align int.coe_cast_add_hom Int.coe_castAddHom
/-- `coe : ℤ → α` as a `RingHom`. -/
def castRingHom ( α : Type _ ) [ NonAssocRing : Type ?u.5860 → Type ?u.5860 α ] : ℤ →+* α where
toFun := Int.cast
map_zero' := cast_zero
map_add' := cast_add
map_one' := cast_one
map_mul' := cast_mul
#align int.cast_ring_hom Int.castRingHom
@[ simp ]
theorem coe_castRingHom [ NonAssocRing : Type ?u.6730 → Type ?u.6730 α ] : ⇑( castRingHom α ) = fun x : ℤ => ( x : α ) :=
rfl : ∀ {α : Sort ?u.7221} {a : α }, a = a
#align int.coe_cast_ring_hom Int.coe_castRingHom
theorem cast_commute [ NonAssocRing : Type ?u.7267 → Type ?u.7267 α ] : ∀ ( m : ℤ ) ( x : α ), Commute : {S : Type ?u.7275} → [inst : Mul S S → S → Prop (↑ m ) x
| (n : ℕ), x => by simpa using n . cast_commute x
| -[ n +1], x => by
simpa only [ cast_negSucc , Commute.neg_left_iff , Commute.neg_right_iff ] using
( n + 1 ). cast_commute (- x )
#align int.cast_commute Int.cast_commute
theorem cast_comm [ NonAssocRing : Type ?u.8746 → Type ?u.8746 α ] ( m : ℤ ) ( x : α ) : ( m : α ) * x = x * m :=
( cast_commute m x ). eq
#align int.cast_comm Int.cast_comm
theorem commute_cast [ NonAssocRing : Type ?u.9094 → Type ?u.9094 α ] ( x : α ) ( m : ℤ ) : Commute : {S : Type ?u.9101} → [inst : Mul S S → S → Prop x m :=
( m . cast_commute x ). symm
#align int.commute_cast Int.commute_cast
theorem cast_mono [ OrderedRing : Type ?u.9314 → Type ?u.9314 α ] : Monotone ( fun x : ℤ => ( x : α )) := by
intro m n h (fun x => ↑x ) m ≤ (fun x => ↑x ) n
rw [ (fun x => ↑x ) m ≤ (fun x => ↑x ) n ← sub_nonneg (fun x => ↑x ) m ≤ (fun x => ↑x ) n ] (fun x => ↑x ) m ≤ (fun x => ↑x ) n at h (fun x => ↑x ) m ≤ (fun x => ↑x ) n
lift n - m to ℕ using h with k hk
rw [ ← sub_nonneg , ← cast_sub , ← hk , cast_ofNat ]
exact k . cast_nonneg
#align int.cast_mono Int.cast_mono
@[ simp ]
theorem cast_nonneg [ OrderedRing : Type ?u.10845 → Type ?u.10845 α ] [ Nontrivial α ] : ∀ { n : ℤ }, ( 0 : α ) ≤ n ↔ 0 ≤ n
| (n : ℕ) => by simp
| -[ n +1] => by
have : -( n : α ) < 1 := lt_of_le_of_lt : ∀ {α : Type ?u.12341} [inst : Preorder α a b c : α }, a ≤ b b < c a < c ( by simp ) zero_lt_one
simpa [( negSucc_lt_zero : ∀ (n : ℕ ), -[ n +1] < 0 n ). not_le : ∀ {α : Type ?u.13528} [inst : Preorder α a b : α }, a < b ¬ b ≤ a not_le , ← sub_eq_add_neg , le_neg ] using this . not_le : ∀ {α : Type ?u.15513} [inst : Preorder α a b : α }, a < b ¬ b ≤ a
#align int.cast_nonneg Int.cast_nonneg
@[ simp , norm_cast ]
theorem cast_le [ OrderedRing : Type ?u.15861 → Type ?u.15861 α ] [ Nontrivial α ] { m n : ℤ } : ( m : α ) ≤ n ↔ m ≤ n := by
rw [ ← sub_nonneg , ← cast_sub , cast_nonneg , sub_nonneg ]
#align int.cast_le Int.cast_le
theorem cast_strictMono [ OrderedRing : Type ?u.17074 → Type ?u.17074 α ] [ Nontrivial α ] : StrictMono ( fun x : ℤ => ( x : α )) :=
strictMono_of_le_iff_le fun _ _ => cast_le . symm : ∀ {a b : Prop }, (a ↔ b b ↔ a
#align int.cast_strict_mono Int.cast_strictMono
@[ simp , norm_cast ]
theorem cast_lt [ OrderedRing : Type ?u.17585 → Type ?u.17585 α ] [ Nontrivial α ] { m n : ℤ } : ( m : α ) < n ↔ m < n :=
cast_strictMono . lt_iff_lt
#align int.cast_lt Int.cast_lt
@[ simp ]
theorem cast_nonpos [ OrderedRing : Type ?u.18196 → Type ?u.18196 α ] [ Nontrivial α ] { n : ℤ } : ( n : α ) ≤ 0 ↔ n ≤ 0 := by
rw [ ← cast_zero , cast_le ]
#align int.cast_nonpos Int.cast_nonpos
@[ simp ]
theorem cast_pos [ OrderedRing : Type ?u.18787 → Type ?u.18787 α ] [ Nontrivial α ] { n : ℤ } : ( 0 : α ) < n ↔ 0 < n := by
rw [ ← cast_zero , cast_lt ]
#align int.cast_pos Int.cast_pos
@[ simp ]
theorem cast_lt_zero [ OrderedRing : Type ?u.19426 → Type ?u.19426 α ] [ Nontrivial α ] { n : ℤ } : ( n : α ) < 0 ↔ n < 0 := by
rw [ ← cast_zero , cast_lt ]
#align int.cast_lt_zero Int.cast_lt_zero
section LinearOrderedRing
variable [ LinearOrderedRing : Type ?u.20902 → Type ?u.20902 α ] { a b : ℤ } ( n : ℤ )
@[ simp , norm_cast ]
theorem cast_min : (↑( min : {α : Type ?u.20049} → [self : Min α α → α → α a b ) : α ) = min : {α : Type ?u.20121} → [self : Min α α → α → α ( a : α ) ( b : α ) :=
Monotone.map_min cast_mono
#align int.cast_min Int.cast_min
@[ simp , norm_cast ]
theorem cast_max : (↑( max : {α : Type ?u.20481} → [self : Max α α → α → α a b ) : α ) = max : {α : Type ?u.20553} → [self : Max α α → α → α ( a : α ) ( b : α ) :=
Monotone.map_max cast_mono
#align int.cast_max Int.cast_max
@[ simp , norm_cast ]
theorem cast_abs : ((| a | : ℤ ) : α ) = |( a : α )| := by simp [ abs_eq_max_neg ]
#align int.cast_abs Int.cast_abs
theorem cast_one_le_of_pos ( h : 0 < a ) : ( 1 : α ) ≤ a := by exact_mod_cast Int.add_one_le_of_lt : ∀ {a b : ℤ }, a < b a + 1 ≤ b h
#align int.cast_one_le_of_pos Int.cast_one_le_of_pos
theorem cast_le_neg_one_of_neg ( h : a < 0 ) : ( a : α ) ≤ - 1 := by
rw [ ← Int.cast_one , ← Int.cast_neg , cast_le ]
exact Int.le_sub_one_of_lt : ∀ {a b : ℤ }, a < b a ≤ b - 1 h
#align int.cast_le_neg_one_of_neg Int.cast_le_neg_one_of_neg
variable ( α ) { n }
theorem cast_le_neg_one_or_one_le_cast_of_ne_zero : n ≠ 0 ↑n ≤ - 1 ∨ 1 ≤ ↑n cast_le_neg_one_or_one_le_cast_of_ne_zero ( hn : n ≠ 0 ) : ( n : α ) ≤ - 1 ∨ 1 ≤ ( n : α ) :=
hn . lt_or_lt . imp : ∀ {a c b d : Prop }, (a → c (b → d a ∨ b c ∨ d cast_le_neg_one_of_neg cast_one_le_of_pos
#align int.cast_le_neg_one_or_one_le_cast_of_ne_zero Int.cast_le_neg_one_or_one_le_cast_of_ne_zero
variable { α } ( n )
theorem nneg_mul_add_sq_of_abs_le_one { x : α } ( hx : | x | ≤ 1 ) : ( 0 : α ) ≤ n * x + n * n := by
have hnx : 0 < n → 0 ≤ x + n := fun hn => by
have := _root_.add_le_add ( neg_le_of_abs_le hx ) ( cast_one_le_of_pos hn )
rwa [ add_left_neg : ∀ {G : Type ?u.30287} [inst : AddGroup G a : G ), - a + a = 0 ] at this
have hnx' : n < 0 → x + n ≤ 0 := fun hn => by
have := _root_.add_le_add ( le_of_abs_le hx ) ( cast_le_neg_one_of_neg hn )
rwa [ add_right_neg : ∀ {G : Type ?u.30732} [inst : AddGroup G a : G ), a + - a = 0 ] at this
rw [ ← mul_add , mul_nonneg_iff ]
rcases lt_trichotomy n 0 with (h | rfl | h) : n < 0 ∨ n = 0 ∨ 0 < n h h | rfl | h : n < 0 ∨ n = 0 ∨ 0 < n rfl h | rfl | h : n < 0 ∨ n = 0 ∨ 0 < n h (h | rfl | h) : n < 0 ∨ n = 0 ∨ 0 < n
· exact Or.inr : ∀ {a b : Prop }, b → a ∨ b ⟨ by exact_mod_cast h . le : ∀ {α : Type ?u.32954} [inst : Preorder α a b : α }, a < b a ≤ b , hnx' h ⟩
· simp [ le_total 0 x ]
· exact Or.inl : ∀ {a b : Prop }, a → a ∨ b ⟨ by exact_mod_cast h . le : ∀ {α : Type ?u.33777} [inst : Preorder α a b : α }, a < b a ≤ b , hnx h ⟩
#align int.nneg_mul_add_sq_of_abs_le_one Int.nneg_mul_add_sq_of_abs_le_one
theorem cast_natAbs : ( n . natAbs : α ) = | n | := by
cases n
· simp
· rw [ abs_eq_natAbs , natAbs_negSucc , cast_succ , cast_ofNat , cast_succ ]
#align int.cast_nat_abs Int.cast_natAbs
end LinearOrderedRing
theorem coe_int_dvd : ∀ [inst : CommRing α m n : ℤ ), m ∣ n ↑m ∣ ↑n coe_int_dvd [ CommRing α ] ( m n : ℤ ) ( h : m ∣ n ) : ( m : α ) ∣ ( n : α ) :=
RingHom.map_dvd : ∀ {α : Type ?u.34999} {β : Type ?u.35000} [inst : Semiring α inst_1 : Semiring β f : α →+* β a b : α },
a ∣ b ↑f a ∣ ↑f b ( Int.castRingHom α ) h
#align int.coe_int_dvd Int.coe_int_dvd : ∀ {α : Type u_1} [inst : CommRing α m n : ℤ ), m ∣ n ↑m ∣ ↑n
end cast
end Int
open Int
namespace AddMonoidHom
variable { A : Type _ : Type (?u.40874+1)}
/-- Two additive monoid homomorphisms `f`, `g` from `ℤ` to an additive monoid are equal
if `f 1 = g 1`. -/
@[ ext high ]
theorem ext_int [ AddMonoid : Type ?u.35268 → Type ?u.35268 A ] { f g : ℤ →+ A } ( h1 : f 1 = g 1 ) : f = g :=
have : f . comp ( Int.ofNatHom : ℕ →+ ℤ ) = g . comp ( Int.ofNatHom : ℕ →+ ℤ ) := ext_nat' _ _ h1
have this' : ∀ (n : ℕ ), ↑f ↑n = ↑g ↑n this' : ∀ n : ℕ , f n = g n := FunLike.ext_iff : ∀ {F : Sort ?u.38882} {α : Sort ?u.38884} {β : α → Sort ?u.38883i : FunLike F α β f g : F },
f = g ↔ ∀ (x : α ), ↑f x = ↑g x . 1 : ∀ {a b : Prop }, (a ↔ b a → b this
ext fun n => match n with
| (n : ℕ) => this' : ∀ (n : ℕ ), ↑f ↑n = ↑g ↑n this' n
| .negSucc n => eq_on_neg _ _ ( this' : ∀ (n : ℕ ), ↑f ↑n = ↑g ↑n this' <| n + 1 )
#align add_monoid_hom.ext_int AddMonoidHom.ext_int : ∀ {A : Type u_1} [inst : AddMonoid A f g : ℤ →+ A ↑f 1 = ↑g 1 f = g
variable [ AddGroupWithOne : Type ?u.40877 → Type ?u.40877 A ]
theorem eq_int_castAddHom ( f : ℤ →+ A ) ( h1 : f 1 = 1 ) : f = Int.castAddHom A :=
ext_int <| by simp [ h1 ]
#align add_monoid_hom.eq_int_cast_hom AddMonoidHom.eq_int_castAddHom
end AddMonoidHom
theorem eq_intCast' [ AddGroupWithOne : Type ?u.43207 → Type ?u.43207 α ] [ AddMonoidHomClass F ℤ α ] ( f : F ) ( h₁ : f 1 = 1 ) :
∀ n : ℤ , f n = n :=
FunLike.ext_iff : ∀ {F : Sort ?u.45310} {α : Sort ?u.45312} {β : α → Sort ?u.45311i : FunLike F α β f g : F },
f = g ↔ ∀ (x : α ), ↑f x = ↑g x . 1 : ∀ {a b : Prop }, (a ↔ b a → b <| ( f : ℤ →+ α ). eq_int_castAddHom h₁
#align eq_int_cast' eq_intCast'
@[ simp ]
theorem Int.castAddHom_int : Int.castAddHom ℤ = AddMonoidHom.id ℤ :=
(( AddMonoidHom.id ℤ ). eq_int_castAddHom rfl : ∀ {α : Sort ?u.46962} {a : α }, a = a ). symm : ∀ {α : Sort ?u.46969} {a b : α }, a = b b = a symm
#align int.cast_add_hom_int Int.castAddHom_int
namespace MonoidHom
variable { M : Type _ : Type (?u.47012+1)} [ Monoid M ]
open Multiplicative
@[ ext ]
theorem ext_mint { f g : Multiplicative : Type ?u.47267 → Type ?u.47267 ℤ →* M } ( h1 : ↑f (↑ofAdd 1 ) = ↑g (↑ofAdd 1 ) h1 : f ( ofAdd 1 ) = g ( ofAdd 1 )) : f = g :=
MonoidHom.toAdditive'' . injective <| AddMonoidHom.ext_int : ∀ {A : Type ?u.48429} [inst : AddMonoid A f g : ℤ →+ A ↑f 1 = ↑g 1 f = g <| Additive.toMul . injective h1 : ↑f (↑ofAdd 1 ) = ↑g (↑ofAdd 1 ) h1
#align monoid_hom.ext_mint MonoidHom.ext_mint
/-- If two `MonoidHom`s agree on `-1` and the naturals then they are equal. -/
@[ ext ]
theorem ext_int { f g : ℤ →* M } ( h_neg_one : ↑f (- 1 = ↑g (- 1 h_neg_one : f (- 1 ) = g (- 1 ))
( h_nat : f . comp Int.ofNatHom . toMonoidHom = g . comp Int.ofNatHom . toMonoidHom ) : f = g := by
ext ( x | x )
· exact ( FunLike.congr_fun : ∀ {F : Sort ?u.50391} {α : Sort ?u.50393} {β : α → Sort ?u.50392i : FunLike F α β f g : F },
f = g ∀ (x : α ), ↑f x = ↑g x h_nat x : _ )
· rw [ Int.negSucc_eq : ∀ (n : ℕ ), -[ n +1] = - (↑n + 1 , h.negSucc ↑f (- (↑x + 1 = ↑g (- (↑x + 1 ← neg_one_mul , h.negSucc ↑f (- 1 * (↑x + 1 = ↑g (- 1 * (↑x + 1 f . map_mul , h.negSucc ↑f (- 1 * ↑f (↑x + 1 = ↑g (- 1 * (↑x + 1 g . map_mul h.negSucc ↑f (- 1 * ↑f (↑x + 1 = ↑g (- 1 * ↑g (↑x + 1 ] h.negSucc ↑f (- 1 * ↑f (↑x + 1 = ↑g (- 1 * ↑g (↑x + 1
congr 1 h.negSucc.e_a ↑f (↑x + 1 = ↑g (↑x + 1
exact_mod_cast ( FunLike.congr_fun : ∀ {F : Sort ?u.51302} {α : Sort ?u.51304} {β : α → Sort ?u.51303i : FunLike F α β f g : F },
f = g ∀ (x : α ), ↑f x = ↑g x h_nat ( x + 1 ) : _ )
#align monoid_hom.ext_int MonoidHom.ext_int
end MonoidHom
namespace MonoidWithZeroHom
variable { M : Type _ : Type (?u.51917+1)} [ MonoidWithZero : Type ?u.51938 → Type ?u.51938 M ]
/-- If two `MonoidWithZeroHom`s agree on `-1` and the naturals then they are equal. -/
@[ ext ]
theorem ext_int { f g : ℤ →*₀ M } ( h_neg_one : ↑f (- 1 = ↑g (- 1 h_neg_one : f (- 1 ) = g (- 1 ))
( h_nat : f . comp Int.ofNatHom . toMonoidWithZeroHom = g . comp Int.ofNatHom . toMonoidWithZeroHom ) :
f = g :=
toMonoidHom_injective <| MonoidHom.ext_int h_neg_one : ↑f (- 1 = ↑g (- 1 h_neg_one <|
MonoidHom.ext ( FunLike.congr_fun : ∀ {F : Sort ?u.53514} {α : Sort ?u.53516} {β : α → Sort ?u.53515i : FunLike F α β f g : F },
f = g ∀ (x : α ), ↑f x = ↑g x h_nat : _ )
#align monoid_with_zero_hom.ext_int MonoidWithZeroHom.ext_int
end MonoidWithZeroHom
/-- If two `MonoidWithZeroHom`s agree on `-1` and the _positive_ naturals then they are equal. -/
theorem ext_int' [ MonoidWithZero : Type ?u.54423 → Type ?u.54423 α ] [ MonoidWithZeroHomClass F ℤ α ] { f g : F }
( h_neg_one : ↑f (- 1 = ↑g (- 1 h_neg_one : f (- 1 ) = g (- 1 )) ( h_pos : ∀ (n : ℕ ), 0 < n ↑f ↑n = ↑g ↑n h_pos : ∀ n : ℕ , 0 < n → f n = g n ) : f = g :=
( FunLike.ext : ∀ {F : Sort ?u.56869} {α : Sort ?u.56870} {β : α → Sort ?u.56868i : FunLike F α β f g : F ),
(∀ (x : α ), ↑f x = ↑g x ) → f = g _ _ ) fun n =>
haveI :=
FunLike.congr_fun : ∀ {F : Sort ?u.56916} {α : Sort ?u.56918} {β : α → Sort ?u.56917i : FunLike F α β f g : F },
f = g ∀ (x : α ), ↑f x = ↑g x
(@ MonoidWithZeroHom.ext_int _ _ ( f : ℤ →*₀ α ) ( g : ℤ →*₀ α ) h_neg_one : ↑f (- 1 = ↑g (- 1 h_neg_one <|
MonoidWithZeroHom.ext_nat (