carrier_inj

Mathlib.FieldTheory.Minpoly.ConjRootClass

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

← MathLib Explorer

English

The map that assigns to x its carrier is injective.

Русский

Отображение x ↦ c.x (carrier) инъективно.

LaTeX

$$Function.Injective (carrier (K := K) (L := L))$$

Lean4

theorem carrier_inj : Function.Injective (carrier (K := K) (L := L)) :=
  by
  intro x y H
  induction x with
  | h x => ?_
  induction y with
  | h y => ?_
  simp_rw [Set.ext_iff, mem_carrier] at H
  rw [← H]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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