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) (↑↑(IsUnit.unit h)⁻¹ (x • m')) = ↑↑(IsUnit.unit h) 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)⁻¹ (x • m') = m'
apply_fun ⇑h.unit.val 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'
⊢ x • m' = ↑↑(IsUnit.unit h) 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) (↑↑(IsUnit.unit h)⁻¹ (x • m')) = ↑↑(IsUnit.unit h) 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'
⊢ x • m' = ↑↑(IsUnit.unit h) m'
rfl