half_moduleEnd_apply_eq_half_smul

English

Applying the inverse of 2 in End_R(M) to x coincides with multiplying x by the inverse of 2 in R.

Русский

Применение обратного 2 в End_R(M) к x совпадает с умножением x на обратное 2 в R.

LaTeX

$$$ ⅟(2 : \mathrm{End}_R(M)) \; x = ⅟(2 : R) \; \cdot x $$$

Lean4

/-- If `2` is invertible in `R`, then applying the inverse of `2` in `End R M` to an element
of `M` is the same as multiplying by the inverse of `2` in `R`. -/
@[simp]
theorem half_moduleEnd_apply_eq_half_smul [Invertible (2 : R)] (x : M) : ⅟(2 : Module.End R M) x = ⅟(2 : R) • x :=
  rfl

Похожие утверждения