Theorems · Theorem · field theory
Algebra.TensorProduct.isField_of_isAlgebraic
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type u_1) [inst_3 : Field K] [inst_4 : Algebra F K] [IsDomain (TensorProduct F E K)], Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F K → IsField (TensorProduct F E K)
If E and K are field extensions of F, one of them is algebraic, such that
E ⊗[F] K is a domain, then E ⊗[F] K is also a field. It is a corollary of
Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective and
IntermediateField.sup_toSubalgebra_of_isAlgebraic.
See Algebra.TensorProduct.isAlgebraic_of_isField for its converse (in an earlier file).
- Defined in
- Mathlib.FieldTheory.LinearDisjoint
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Algebrastatement and proof · cited by 11,388
- Fieldstatement and proof · cited by 7,404
- Algebra.algebraMapproof · cited by 4,706
- AlgHomproof · cited by 3,236
- TensorProductstatement and proof · cited by 2,545
- IsDomainstatement and proof · cited by 2,196
- AlgEquivproof · cited by 1,681
- Algebra.IsAlgebraicstatement and proof · cited by 322
- RingHom.injectiveproof · cited by 187
- AlgHom.rangeproof · cited by 169
- IntermediateField.toSubalgebraproof · cited by 134
Cited by2
Results whose statement or proof uses this declaration.
- IntermediateField.LinearDisjoint.isField_of_isAlgebraicproof · cited by 1
- IntermediateField.LinearDisjoint.isField_of_isAlgebraic'proof · cited by 0