mem_span_singleton — Mathlib

English

For y ∈ M, x ∈ R ∙ y iff ∃ a ∈ R with a • y = x.

Русский

Для любых y ∈ M верно: x ∈ R ∙ y тогда и только тогда, когда существует a ∈ R такое, что a • y = x.

LaTeX

$$$$ x \\in R \\cdot y \\iff \\exists a \\in R, a \\cdot y = x. $$$$

Lean4

theorem mem_span_singleton {y : M} : (x ∈ R ∙ y) ↔ ∃ a : R, a • y = x :=
  ⟨fun h => by
    refine span_induction ?_ ?_ ?_ ?_ h
    · rintro y (rfl | ⟨⟨_⟩⟩)
      exact ⟨1, by simp⟩
    · exact ⟨0, by simp⟩
    · rintro _ _ - - ⟨a, rfl⟩ ⟨b, rfl⟩
      exact ⟨a + b, by simp [add_smul]⟩
    · rintro a _ - ⟨b, rfl⟩
      exact ⟨a * b, by simp [smul_smul]⟩, by rintro ⟨a, y, rfl⟩; exact smul_mem _ _ (subset_span <| by simp)⟩

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