lmul_isUnit_iff — Mathlib

English

For any x ∈ A, the endomorphism given by left multiplication by x is a unit in End_R(A) if and only if x is a unit in A.

Русский

Для любого x ∈ A концевой оператор левого умножения на x является обратимым в End_R(A) тогда и только тогда, когда x обратим в A.

LaTeX

$$$\IsUnit(\text{lmul }R\ A\ x) \;\iff\; \IsUnit(x).$$$

Lean4

theorem _root_.Algebra.lmul_isUnit_iff {x : A} : IsUnit (Algebra.lmul R A x) ↔ IsUnit x :=
  by
  rw [Module.End.isUnit_iff, Iff.comm]
  exact IsUnit.isUnit_iff_mulLeft_bijective

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