English
As in the previous statement, with the swapped equality: m' = (h.unit)^{-1} m if and only if m = x · m', under the same hypothesis that the endomorphism corresponding to x is a unit.
Русский
Как и в предыдущем утверждении, при том же предположении, что соответствующее x единично как линейное преобразование, выполняется m' = (h.unit)^{-1} m тогда и только тогда, когда m = x · m'.
LaTeX
$$$\forall x\in R\; (\text{If }\; \mathrm{algebraMap}_{R}(\mathrm{Module.End}_{S} M)(x)\ \text{is a unit}),\; m,m'\in M:\; m' = (\mathrm{algebraMap}_{R}(\mathrm{Module.End}_{S} M)(x))^{-1} m \iff m = x \cdot m'. $$$
Lean4
theorem algebraMap_isUnit_inv_apply_eq_iff' {x : R} (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) :
m' = (↑h.unit⁻¹ : Module.End S M) m ↔ m = x • m'
where
mp H := H ▸ (isUnit_apply_inv_apply_of_isUnit h m).symm
mpr
H :=
H.symm ▸ by
apply_fun (↑h.unit : M → M) using ((isUnit_iff _).mp h).injective
simpa using isUnit_apply_inv_apply_of_isUnit h (x • m') |>.symm
