instSMulCommClass_1 — Mathlib

English

There is a SMulCommClass for R and R' acting on the Ore localization X[S⁻¹], i.e., the actions of R and R' commute on the localized object.

Русский

Существует SMulCommClass для R и R' действующих на X[S⁻¹], то есть действия R и R' коммутируют на локализованном предмете.

LaTeX

$$$\\text{SMulCommClass}(R,R',X[S^{-1}]).$$$

Lean4

@[to_additive]
instance [SMulCommClass R M M] : SMulCommClass R M[S⁻¹] X[S⁻¹] where
  smul_comm r x
    y :=
    by
    cases x with
    | _ r₁ s₁
    cases y with
    | _ r₂ s₂
    rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, smul_smul, smul_smul, mul_div_one,
      oreDiv_mul_char _ _ _ _ (r • 1) s₁ (by simp), mul_one]
    simp

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