English
If A ⊗_R B is a field, then A and B are linearly disjoint over R.
Русский
Если A ⊗_R B — поле, то A и B линейно независимы над R.
LaTeX
$$$\\text{IsField}(A \\otimes_R B) \\Rightarrow A \\perp_L B$$$
Lean4
/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
linearly disjoint and such that `A ⊔ B = S`, then `norm` and `algebraMap` commutes.
-/
theorem norm_algebraMap (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) [Module.Free R B] [Module.Finite R B] (x : B) :
Algebra.norm A (algebraMap B S x) = algebraMap R A (Algebra.norm R x) := by
simp_rw [Algebra.norm_eq_matrix_det (Module.Free.chooseBasis R B),
Algebra.norm_eq_matrix_det (H.basisOfBasisRight H' (Module.Free.chooseBasis R B)),
leftMulMatrix_basisOfBasisRight_algebraMap, RingHom.map_det]
