case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
by_cases h : s ∈ spectrum R a
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (↑↑ₐ s - a)
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
rw [mem_iff] at h
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse ((r⁻¹ • s) • 1 - r⁻¹ • a)
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (↑↑ₐ s - a)
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
simp only [resolvent, Algebra.algebraMap_eq_smul_one] at *
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (s • 1 - a))
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse ((r⁻¹ • s) • 1 - r⁻¹ • a)
rw [smul_assoc, ← smul_sub]
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
h' : ¬IsUnit (r⁻¹ • (s • 1 - a))
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (s • 1 - a))
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (s • 1 - a))
have h' : ¬IsUnit (r⁻¹ • (s • (1 : A) - a)) := fun hu =>
  h (by simpa only [smul_inv_smul] using IsUnit.smul r hu)
no goals
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
h' : ¬IsUnit (r⁻¹ • (s • 1 - a))
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (s • 1 - a))
simp only [Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ h', smul_zero]
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
hu : IsUnit (r⁻¹ • (s • 1 - a))
⊢ IsUnit (s • 1 - a)
simpa only [smul_inv_smul] using IsUnit.smul r hu
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
⊢ r • Ring.inverse (↑↑ₐ s - a) = Ring.inverse (↑↑ₐ (r⁻¹ • s) - r⁻¹ • a)
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
simp only [resolvent]
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
h' : IsUnit (r • ↑↑ₐ (r⁻¹ • s) - a)
⊢ r • Ring.inverse (↑↑ₐ s - a) = Ring.inverse (↑↑ₐ (r⁻¹ • s) - r⁻¹ • a)
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
⊢ r • Ring.inverse (↑↑ₐ s - a) = Ring.inverse (↑↑ₐ (r⁻¹ • s) - r⁻¹ • a)
have h' : IsUnit (r • algebraMap R A (r⁻¹ • s) - a) := by
  simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using not_mem_iff.mp h
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
h' : IsUnit (r • ↑↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑(IsUnit.unit (_ : IsUnit (↑↑ₐ s - a)))⁻¹ = r • ↑(IsUnit.unit h')⁻¹
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
h' : IsUnit (r • ↑↑ₐ (r⁻¹ • s) - a)
⊢ r • Ring.inverse (↑↑ₐ s - a) = Ring.inverse (↑↑ₐ (r⁻¹ • s) - r⁻¹ • a)
rw [← h'.subInvSMul_val, ← (not_mem_iff.mp h).unit_spec, Ring.inverse_unit, Ring.inverse_unit,
  ←h'.subInvSMul.inv_eq_val_inv, h'.subInvSMul_inv]
no goals
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
h' : IsUnit (r • ↑↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑(IsUnit.unit (_ : IsUnit (↑↑ₐ s - a)))⁻¹ = r • ↑(IsUnit.unit h')⁻¹
simp only [Algebra.algebraMap_eq_smul_one, smul_assoc, smul_inv_smul]
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
⊢ IsUnit (r • ↑↑ₐ (r⁻¹ • s) - a)
simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using not_mem_iff.mp h