Theorems · Theorem · commutative algebra

Subalgebra.LinearDisjoint.isDomain

∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S}, A.LinearDisjoint B → ∀ [IsDomain S], IsDomain (TensorProduct R ↥A ↥B)

If A and B are subalgebras in a domain S over R, and if they are linearly disjoint, then A ⊗[R] B is also a domain.

Defined in

Mathlib.RingTheory.LinearDisjoint

Cited by

2 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraIsDomain