inf_toSubalgebra — Mathlib

English

The subalgebra associated to the intersection equals the intersection of the associated subalgebras.

Русский

Подалгебра, связанная с пересечением, равна пересечению соответствующих подпалгебр.

LaTeX

$$$ (S \\cap T).toSubalgebra = S.toSubalgebra \\cap T.toSubalgebra $$$

Lean4

@[simp]
theorem inf_toSubalgebra (S T : IntermediateField F E) : (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra :=
  rfl

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