Commit 2024-02-21 14:19 c63ddc25

View on Github →

feat: unitary elements are normal (#10778)

Estimated changes

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

Modified Mathlib/Algebra/Star/Unitary.lean

added theorem isStarNormal_of_mem_unitary

added theorem unitary.toUnits_injective

deleted theorem unitary.to_units_injective