R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (r⁻¹ • 1 - ↑a⁻¹)
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : ↑r ∈ resolventSet R ↑a
⊢ ↑r⁻¹ ∈ resolventSet R ↑a⁻¹
rw [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, ← Units.smul_def] at h ⊢
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (r • ↑a⁻¹ - 1)
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (r⁻¹ • 1 - ↑a⁻¹)
rw [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv, IsUnit.sub_iff]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ IsUnit (r • ↑a⁻¹ - 1)
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (r • ↑a⁻¹ - 1)
have h₁ : (a : A) * (r • (↑a⁻¹ : A) - 1) = r • (1 : A) - a := by
  rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
⊢ IsUnit (r • ↑a⁻¹ - 1)
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ IsUnit (r • ↑a⁻¹ - 1)
have h₂ : (r • (↑a⁻¹ : A) - 1) * a = r • (1 : A) - a := by
  rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
hcomm : Commute (↑a) (r • ↑a⁻¹ - 1)
⊢ IsUnit (r • ↑a⁻¹ - 1)
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
⊢ IsUnit (r • ↑a⁻¹ - 1)
have hcomm : Commute (a : A) (r • (↑a⁻¹ : A) - 1) := by rwa [← h₂] at h₁
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
hcomm : Commute (↑a) (r • ↑a⁻¹ - 1)
⊢ IsUnit (r • ↑a⁻¹ - 1)
exact (hcomm.isUnit_mul_iff.mp (h₁.symm ▸ h)).2
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
⊢ Commute (↑a) (r • ↑a⁻¹ - 1)
rwa [← h₂] at h₁