carrier_zero

Mathlib.FieldTheory.Minpoly.ConjRootClass

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

English

Membership of x in c.carrier is equivalent to mk K x = c.

Русский

Принадлежность x к c.carrier эквивалентна mk K x = c.

LaTeX

$$x \in c.carrier \iff mk K x = c$$

Lean4

@[simp]
theorem carrier_zero : (0 : ConjRootClass K L).carrier = {0} := by ext;
  rw [mem_carrier, mk_eq_zero_iff, Set.mem_singleton_iff]

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

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

Разделы

Аффилиация

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