case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
⊢ ↑φ x = ↑ψ x
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
⊢ φ = ψ
ext x
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
this : x - ↑(algebraMap 𝕜 A) (↑ψ x) ∈ RingHom.ker φ
⊢ ↑φ x = ↑ψ x
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
⊢ ↑φ x = ↑ψ x
have : x - algebraMap 𝕜 A (ψ x) ∈ RingHom.ker φ := by
  simpa only [h, RingHom.mem_ker, map_sub, AlgHomClass.commutes] using sub_self (ψ x)
no goals
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
⊢ x - ↑(algebraMap 𝕜 A) (↑ψ x) ∈ RingHom.ker φ
simpa only [h, RingHom.mem_ker, map_sub, AlgHomClass.commutes] using sub_self (ψ x)
no goals
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
this : x - ↑(algebraMap 𝕜 A) (↑ψ x) ∈ RingHom.ker φ
⊢ ↑φ x = ↑ψ x
rwa [RingHom.mem_ker, map_sub, AlgHomClass.commutes, sub_eq_zero] at this