Theorem IsUnit.mem_unitary_of_mul_star_self

Modification history

2024-02-22 18:08
Mathlib/Algebra/Star/Unitary.lean
feat: add `IsUnit.mem_unitary_of_star_mul_self` and protect some `.star` lemmas (#10855)
Added IsUnit.mem_unitary_of_mul_star_selfView on Github →