top_toSubring — Mathlib

English

The underlying Subring of the top Subalgebra equals the top Subring (when the base rings are suitable).

Русский

Подкольцо нижнего уровня подалгебры равно верхнему подкольцу (при соответствующих условиях на базовые кольца).

LaTeX

$$$ (\top : Subalgebra R A).toSubring = \top $$$

Lean4

@[simp]
theorem top_toSubring {R A : Type*} [CommRing R] [Ring A] [Algebra R A] : (⊤ : Subalgebra R A).toSubring = ⊤ :=
  rfl

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