R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
h : IsUnit (↑(algebraMap R (End R M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h) m' = ↑↑(IsUnit.unit h) (↑↑(IsUnit.unit h)⁻¹ (x • m'))
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
h : IsUnit (↑(algebraMap R (End R M)) x)
m m' : M
H : m = x • m'
⊢ m' = ↑↑(IsUnit.unit h)⁻¹ (x • m')
apply_fun (↑h.unit : M → M) using ((Module.End_isUnit_iff _).mp h).injective
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
h : IsUnit (↑(algebraMap R (End R M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h) m' = x • m'
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
h : IsUnit (↑(algebraMap R (End R M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h) m' = ↑↑(IsUnit.unit h) (↑↑(IsUnit.unit h)⁻¹ (x • m'))
erw [End_isUnit_apply_inv_apply_of_isUnit]
no goals
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
h : IsUnit (↑(algebraMap R (End R M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h) m' = x • m'
rfl