case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ (∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g') → g = g'

case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ g = g' → ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ (∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g') ↔ g = g'
constructor
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
⊢ g = g'
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ (∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g') → g = g'
intro hg
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
⊢ ↑g x = ↑g' x
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
⊢ g = g'
ext x : 1
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
⊢ ∀ (n : ℕ), ↑(toZModPow n) (↑g x) = ↑(toZModPow n) (↑g' x)
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
⊢ ↑g x = ↑g' x
apply ext_of_toZModPow.mp
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
n : ℕ
⊢ ↑(toZModPow n) (↑g x) = ↑(toZModPow n) (↑g' x)
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
⊢ ∀ (n : ℕ), ↑(toZModPow n) (↑g x) = ↑(toZModPow n) (↑g' x)
intro n
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
n : ℕ
⊢ ↑(RingHom.comp (toZModPow n) g) x = ↑(RingHom.comp (toZModPow n) g') x
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
n : ℕ
⊢ ↑(toZModPow n) (↑g x) = ↑(toZModPow n) (↑g' x)
show (toZModPow n).comp g x = (toZModPow n).comp g' x
no goals
case mp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
n : ℕ
⊢ ↑(RingHom.comp (toZModPow n) g) x = ↑(RingHom.comp (toZModPow n) g') x
rw [hg n]
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g : R →+* ℤ_[p]
n✝ : ℕ
⊢ RingHom.comp (toZModPow n✝) g = RingHom.comp (toZModPow n✝) g
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ g = g' → ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
rintro rfl _
no goals
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g : R →+* ℤ_[p]
n✝ : ℕ
⊢ RingHom.comp (toZModPow n✝) g = RingHom.comp (toZModPow n✝) g
rfl