mem_carrier

Mathlib.FieldTheory.Minpoly.ConjRootClass

URI: https://scilib.ai/kg/mathlib#ConjRootClass.mem_carrier

English

For c ∈ ConjRootClass K L, c.carrier is the set of elements of L represented by c.

Русский

Для c ∈ ConjRootClass K L множество c.carrier состоит из элементов L, представленных c.

LaTeX

$$def carrier (c : ConjRootClass K L) : Set L := mk K ⁻¹' { c }$$

Lean4

@[simp]
theorem mem_carrier {x : L} {c : ConjRootClass K L} : x ∈ c.carrier ↔ mk K x = c :=
  Iff.rfl

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

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

Разделы

Аффилиация

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