conjneg_inj

Mathlib.Algebra.Star.Conjneg

URI: https://scilib.ai/kg/mathlib#conjneg_inj

English

Conjneg as a map is injective: conjneg f = conjneg g implies f = g.

Русский

Отображение conjneg инъективно: conjneg f = conjneg g тогда и только тогда f = g.

LaTeX

$$$\\text{conjneg\\_inj}:\\; \\text{conjneg } f = \\text{conjneg } g \\iff f = g.$$$

Lean4

@[simp]
theorem conjneg_inj : conjneg f = conjneg g ↔ f = g :=
  conjneg_injective.eq_iff

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

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

Разделы

Аффилиация

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