Commit 2024-11-13 07:59 5b7d4f67

View on Github →

feat: some results on dimension of field adjoin (#18515) In Mathlib/FieldTheory/Adjoin.lean:

  • IntermediateField.rank_sup_le_of_isAlgebraic: if A and B are intermediate fields, and at least one them are algebraic, then the rank of A ⊔ B is less than or equal to the product of that of A and B. (Note that this result is also true without algebraic assumption, but the proof becomes very complicated, and which is out of scope of this PR.)
  • IntermediateField.finrank_sup_le: if A and B are intermediate fields, then the Module.finrank of A ⊔ B is less than or equal to the product of that of A and B. Move the result Subalgebra.[fin]rank_sup_le_of_free from Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean to a new file Mathlib/RingTheory/Adjoin/Dimension.lean, as their proofs don't use tensor mulMap anymore.

Estimated changes