Mathlib Changelog
v4
Changelog
About
Github
Theorem
IsUnit.mem_unitary_iff_star_mul_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_star_mul_self
View on Github →