bot_left — Mathlib

English

For any A, A.LinearDisjoint ⊥ holds; the image of R in S is disjoint from any A.

Русский

Для любой A выполняется A.LinearDisjoint ⊥; образ R в S линейно дизъюнктен с любым A.

LaTeX

$$$(A) LinearDisjoint (\bot)$$$

Lean4

/-- The image of `R` in `S` is linearly disjoint with any other subalgebras. -/
theorem bot_left : (⊥ : Subalgebra R S).LinearDisjoint B :=
  by
  rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]
  exact Submodule.LinearDisjoint.one_left _

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