coe_copy

Mathlib.FieldTheory.IntermediateField.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.coe_copy

English

Two intermediate fields are equal if they have the same elements.

Русский

Два промежуточных поля равны, если совпадают их элементы.

LaTeX

$$$\forall S,T \in \operatorname{IntermediateField}(K,L),\ (\forall x \in L,\ x \in S \iff x \in T) \Rightarrow S = T$$$

Lean4

@[simp]
theorem coe_copy (S : IntermediateField K L) (s : Set L) (hs : s = ↑S) : (S.copy s hs : Set L) = s :=
  rfl

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

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

Разделы

Аффилиация

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