mk_ideal_smul — Mathlib

English

For a, b in R and x in torsionBy(R, M, a), the action of the class of b in the quotient R/(R a) on x coincides with the ordinary action by b on x.

Русский

Для элементов a, b в R и x в torsionBy(R, M, a) действие класса b в кольце-куотьента R/(R a) на x совпадает с обычным действием b на x.

LaTeX

$$((Ideal.Quotient.mk (Ideal.span { a })) b) • x = b • x for all a,b ∈ R, x ∈ torsionBy(R,M,a).$$

Lean4

@[simp]
theorem mk_ideal_smul (a b : R) (x : torsionBy R M a) : (Ideal.Quotient.mk (Ideal.span { a })) b • x = b • x :=
  rfl

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