mem_iff

Mathlib.Algebra.Star.SelfAdjoint

URI: https://scilib.ai/kg/mathlib#selfAdjoint.mem_iff

Lean4

theorem mem_iff {x : R} : x ∈ selfAdjoint R ↔ star x = x :=
  by
  rw [← AddSubgroup.mem_carrier]
  exact Iff.rfl

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

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

Разделы

Аффилиация

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