instInvertibleEndOfNat — Mathlib

English

If 2 is invertible in R, then the endomorphism 2 on M is invertible, with a natural explicit inverse.

Русский

Если 2 обращаемо в R, то концевой эндоморфизм 2 на M обращаем, с явным обратным отображением.

LaTeX

$$$ \text{Invertible }(2 : \mathrm{End}_R(M)) $$$

Lean4

/-- If `2` is invertible in `R`, then it is also invertible in `End R M`. -/
instance [Invertible (2 : R)] : Invertible (2 : Module.End R M)
    where
  invOf := (⟨⅟2, Set.invOf_mem_center (Set.ofNat_mem_center _ _)⟩ : Submonoid.center R) • (1 : Module.End R M)
  invOf_mul_self := by
    ext m
    dsimp [Submonoid.smul_def]
    rw [← ofNat_smul_eq_nsmul R, invOf_smul_smul (2 : R) m]
  mul_invOf_self := by
    ext m
    dsimp [Submonoid.smul_def]
    rw [← ofNat_smul_eq_nsmul R, smul_invOf_smul (2 : R) m]

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