toSubalgebra_lt_toSubalgebra — Mathlib

English

The strict order on intermediate fields corresponds to strict inclusion on their Subalgebras.

Русский

Строгий порядок над промежуточными полями соответствует строгому включению их подалгебр.

LaTeX

$$$ S.toSubalgebra < S'.toSubalgebra \\iff S < S' $$$

Lean4

@[simp]
theorem toSubalgebra_lt_toSubalgebra {S S' : IntermediateField K L} : S.toSubalgebra < S'.toSubalgebra ↔ S < S' :=
  Iff.rfl

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