Commit 2025-05-13 23:40 40fea086

View on Github →

feat: promote mem_unitary_of_star_mul_self to an Iff (#24867)

Estimated changes

Modified Mathlib/Algebra/Star/Unitary.lean

added theorem IsUnit.mem_unitary_iff_mul_star_self

added theorem IsUnit.mem_unitary_iff_star_mul_self

deleted theorem IsUnit.mem_unitary_of_mul_star_self

deleted theorem IsUnit.mem_unitary_of_star_mul_self