mem_one — Mathlib

English

The image of any r ∈ R under the algebra map lies in the unit submodule: algebraMap R A r ∈ (1 : Submodule R A).

Русский

Образ элемента r ∈ R под алгебраическим отображением лежит в единичном подпмодуле: algebraMap R A r ∈ (1 : Submodule R A).

LaTeX

$$$ algebraMap R A r \in (1 : Submodule R A) $$$

Lean4

@[simp]
theorem mem_one {x : A} : x ∈ (1 : Submodule R A) ↔ ∃ y, algebraMap R A y = x := by simp [one_eq_range]

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