English
From a unit condition on r • s − a one obtains a unit of the form s − r⁻¹ a, giving a way to construct units from units via a shift.
Русский
Из условия единичности на r • s − a следует единичность вида s − r⁻¹ a, давая способ перейти от единицы к единице через сдвиг.
LaTeX
$$$\text{Given } h:\,\operatorname{IsUnit}(r \cdot s - a) \text{, construct } (s - r^{-1} a) \in A^{\times}$$$
Lean4
/-- The unit `1 - r⁻¹ • a` constructed from `r • 1 - a` when the latter is a unit. -/
@[simps]
noncomputable def subInvSMul {r : Rˣ} {s : R} {a : A} (h : IsUnit <| r • ↑ₐ s - a) : Aˣ
where
val := ↑ₐ s - r⁻¹ • a
inv := r • ↑h.unit⁻¹
val_inv := by rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]
inv_val := by rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]
