sup_toSubfield — Mathlib

English

The subfield corresponding to the join of two intermediate fields equals the join of the corresponding subfields.

Русский

Подполе, соответствующее объединению двух промежуточных полей, равно объединению соответствующих подпольей.

LaTeX

$$$ (S \\oplus T).toSubfield = S.toSubfield \\oplus T.toSubfield $$$

Lean4

@[simp]
theorem sup_toSubfield (S T : IntermediateField F E) : (S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield :=
  by
  rw [← S.toSubfield.closure_eq, ← T.toSubfield.closure_eq, ← Subfield.closure_union]
  simp_rw [sup_def, adjoin_toSubfield, coe_toSubfield]
  congr 1
  rw [Set.union_eq_right]
  rintro _ ⟨x, rfl⟩
  exact Set.mem_union_left _ (algebraMap_mem S x)

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