English
Let A and B be subalgebras of a commutative R-algebra S. Then A and B are linearly disjoint over R if and only if the natural multiplication map A ⊗_R B → S is injective.
Русский
Пусть A и B — подалгебры коммутативной R-алгебры S. Тогда A и B линейно несовместны над R тогда и только тогда, когда естественный отображение умножения A ⊗_R B → S инъективно.
LaTeX
$$$A \\text{ and } B \\text{ are linearly disjoint over } R \\iff \\operatorname{Injective}(A \\otimes_R B \\xrightarrow{mulMap} S)$$$
Lean4
/-- Two subalgebras `A`, `B` in a commutative ring are linearly disjoint if and only if
`Subalgebra.mulMap A B` is injective. -/
theorem linearDisjoint_iff_injective : A.LinearDisjoint B ↔ Function.Injective (A.mulMap B) :=
by
rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]
rfl
