restrictScalars_normal — Mathlib

English

For a tower F ⊂ K ⊂ L with E a normal extension over F and IsScalarTower F K L, the normality of E over F is equivalent to the normality of E restricted scalars to F over E.

Русский

Пусть имеется разложение полей F ⊂ K ⊂ L и E — нормальное расширение над F. При условии IsScalarTower F K L нормальность E над F эквивалентна нормальности E после ограничения скаляр на F.

LaTeX

$$$\text{Normal } F (E|_F) \quad\leftrightarrow\quad \text{Normal } F E,$$$

Lean4

@[simp]
theorem restrictScalars_normal {E : IntermediateField K L} : Normal F (E.restrictScalars F) ↔ Normal F E :=
  Iff.rfl

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