Theorem unitary.mem_iff_self_mul_star

Modification history

2023-01-09 16:13
Mathlib/Algebra/Star/Unitary.lean
feat: Port Algebra.Star.Unitary (#1436)
Added unitary.mem_iff_self_mul_starView on Github →