toSpanNonzeroSingleton_symm_apply_smul

English

Let m be an element of the span R·x. Then applying the inverse of the span‑to‑R isomorphism and multiplying by x recovers m, i.e., the inverse map undoes the embedding by x.

Русский

Пусть m принадлежит span_R{ x }. Тогда применение обратного отображения из span в R и умножение на x восстанавливают элемент: (toSpanNonzeroSingleton R M x h)⁻¹(m) · x = m.

LaTeX

$$$ (toSpanNonzeroSingleton R M x h)^{-1}(m) \cdot x = m, \quad m \in R \cdot x. $$$

Lean4

@[simp]
theorem toSpanNonzeroSingleton_symm_apply_smul (m : R ∙ x) : (toSpanNonzeroSingleton R M x h).symm m • x = m :=
  congrArg Subtype.val <| apply_symm_apply (toSpanNonzeroSingleton R M x h) m

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