quotTorsionOfEquivSpanSingleton_apply_mk

English

Under the isomorphism quotTorsionOfEquivSpanSingleton, the image of the class of a in the quotient is the scalar a times the vector x in the span of x.

Русский

Под этим изоморфизмом образ класса a в фактор-пространстве равен a · x внутри подпространства R · x.

LaTeX

$$image( (Q) (Quotient.mk a) ) = a · x ∈ R · x$$

Lean4

@[simp]
theorem quotTorsionOfEquivSpanSingleton_apply_mk (x : M) (a : R) :
    quotTorsionOfEquivSpanSingleton R M x (Submodule.Quotient.mk a) = a • ⟨x, Submodule.mem_span_singleton_self x⟩ :=
  rfl

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