conjneg_ne_conjneg

Mathlib.Algebra.Star.Conjneg

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

English

conjneg f ≠ conjneg g if and only if f ≠ g.

Русский

conjneg f ≠ conjneg g тогда и только если f ≠ g.

LaTeX

$$$\\text{conjneg}f \\neq \\text{conjneg}g \\iff f \\neq g$$$

Lean4

theorem conjneg_ne_conjneg : conjneg f ≠ conjneg g ↔ f ≠ g :=
  conjneg_injective.ne_iff

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

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

Разделы

Аффилиация

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