smul_sub_iff_sub_inv_smul — Mathlib

English

For a group G acting on a ring R with a scalar tower and SMulCommClass, the element r • 1_R − a is a unit iff 1_R − r⁻¹ • a is a unit, for r ∈ G and a ∈ R.

Русский

При действии группы G на кольцо R с тензорной структурой и совместностью действий, элемент r • 1_R − a является единицей тогда и только тогда, когда 1_R − r⁻¹ • a является единицей, для r ∈ G и a ∈ R.

LaTeX

$$$\\IsUnit(r \\cdot 1_R - a) \\iff \\IsUnit(1 - r^{-1} \\cdot a)$$$

Lean4

theorem smul_sub_iff_sub_inv_smul [Group G] [Monoid R] [AddGroup R] [DistribMulAction G R] [IsScalarTower G R R]
    [SMulCommClass G R R] (r : G) (a : R) : IsUnit (r • (1 : R) - a) ↔ IsUnit (1 - r⁻¹ • a) := by
  rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]

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