isDomain — Mathlib

English

If A and L are linearly disjoint over F, then A ⊗F L is a domain.

Русский

Если A и L линейно независимы над F, то A ⊗F L является областью.

LaTeX

$$$\text{IsDomain}(\,A \otimes_F L\,)$$$

Lean4

/-- If `A` and `L` are linearly disjoint over `F`, then `A ⊗[F] L` is a domain. -/
theorem isDomain (H : A.LinearDisjoint L) : IsDomain (A ⊗[F] L) :=
  have : IsDomain (A ⊗[F] _) := Subalgebra.LinearDisjoint.isDomain H
  (Algebra.TensorProduct.congr (AlgEquiv.refl : A ≃ₐ[F] A)
      (AlgEquiv.ofInjective (IsScalarTower.toAlgHom F L E) (RingHom.injective _))).toMulEquiv.isDomain

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