closure_eq

Mathlib.Algebra.Field.Subfield.Basic

URI: https://scilib.ai/kg/mathlib#Subfield.closure_eq

English

The closure of a subfield S equals S itself.

Русский

Замыкание подполя S равно самому S.

LaTeX

$$closure(S) = S$$

Lean4

/-- Closure of a subfield `S` equals `S`. -/
@[simp]
theorem closure_eq (s : Subfield K) : closure (s : Set K) = s :=
  (Subfield.gi K).l_u_eq s

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru