normalClosure_le_iff_of_normal — Mathlib

English

normalClosure F K1 L ≤ K2 if and only if K1 ≤ K2, provided Normal F L.

Русский

normalClosure F K1 L ≤ K2 тогда, когда K1 ≤ K2, при условии Normal F L.

LaTeX

$$$\operatorname{normalClosure} F K_1 L \le K_2 \iff K_1 \le K_2$$$

Lean4

@[simp]
theorem normalClosure_le_iff_of_normal {K₁ K₂ : IntermediateField F L} [Normal F K₂] :
    normalClosure F K₁ L ≤ K₂ ↔ K₁ ≤ K₂ := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [normalClosure_le_iff] at h
    simpa only [fieldRange_val] using h K₁.val
  · rw [← normalClosure_of_normal K₂]
    exact normalClosure_mono K₁ K₂ h

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