one_left — Mathlib

English

The image of R in S, i.e., the submodule generated by 1, is linearly disjoint with any N.

Русский

Образ R в S, порожденный 1, линейно несовместен с любым N.

LaTeX

$$(1 : Submodule R S).LinearDisjoint N$$

Lean4

/-- The image of `R` in `S` is linearly disjoint with any other submodules. -/
theorem one_left : (1 : Submodule R S).LinearDisjoint N :=
  by
  rw [linearDisjoint_iff, ← Algebra.toSubmodule_bot, mulMap_one_left_eq]
  exact N.injective_subtype.comp N.lTensorOne.injective

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