Theorem Units.unitary_eq

feat: `a * b⁻¹` for `a b : Aˣ` is unitary if `star a * a = star b * b` (#24858)