Theorem IsUnit.mem_unitary_iff_mul_star_self

Modification history

2025-05-13 23:40
Mathlib/Algebra/Star/Unitary.lean
feat: promote `mem_unitary_of_star_mul_self` to an `Iff` (#24867)
Added IsUnit.mem_unitary_iff_mul_star_selfView on Github →