English
If f, r, a, v, and a relation hv encode a unit, then the awayLift applied to mk a with r^j yields a product f(a) v^j.
Русский
Если задано отображение f, элемент r, элемент a и связанное с ним отношение hv, то применение awayLift к mk(a, r^j) даёт произведение f(a) на v^j.
LaTeX
$$$\mathrm{awayLift}(f,r)(\mathrm{mk}\;a\;\langle r^j, j, rfl \rangle) = f(a) \cdot v^j$$$
Lean4
theorem awayLift_mk {A : Type*} [CommSemiring A] (f : R →+* A) (r : R) (a : R) (v : A) (hv : f r * v = 1) (j : ℕ) :
Localization.awayLift f r (isUnit_iff_exists_inv.mpr ⟨v, hv⟩) (Localization.mk a ⟨r ^ j, j, rfl⟩) = f a * v ^ j :=
by
simp [Localization.mk_eq_mk', awayLift, Away.lift, IsLocalization.lift_mk', Units.mul_inv_eq_iff_eq_mul,
IsUnit.liftRight, mul_assoc, ← mul_pow, (mul_comm _ _).trans hv]
