Commit 2023-12-13 19:05 39229b7d

View on Github →

feat(FieldTheory/IntermediateField): generalize eq_of_le_of_finrank_{le|eq} (#8873)

  • generalize IntermediateField.eq_of_le_of_finrank_{le|eq}: the condition FiniteDimensional K L is generalized to FiniteDimensional K E (credits: @riccardobrasca)
  • generalize IntermediateField.eq_of_le_of_finrank_{le|eq}': the condition FiniteDimensional K L is generalized to FiniteDimensional F L (original proof credits: @riccardobrasca)
  • add Subalgebra.eq_of_le_of_finrank_{le|eq}
  • add IntermediateField.extendScalars and its basic properties

Estimated changes