torsionBySet_span_singleton_eq — Mathlib

English

Torsion by the R-span of a is equal to torsion by a: torsionBySet(R, M, (R ∙ a)) = torsionBy(R, M, a).

Русский

Торион по линейному порожденному a совпадает с торионом по a: torsionBySet(R, M, R ∙ a) = torsionBy(R, M, a).

LaTeX

$$$\mathrm{torsionBySet}\,R\,M\, (R \cdot a) = \mathrm{torsionBy}\,R\,M\, a$$$

Lean4

theorem torsionBySet_span_singleton_eq : torsionBySet R M (R ∙ a) = torsionBy R M a :=
  (torsionBySet_eq_torsionBySet_span _).symm.trans <| torsionBySet_singleton_eq _

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