Commit 2025-10-29 21:09 c43cec3d

View on Github →

chore: move results from unitary namespace to Unitary (#30697) All results living in the unitary namespace is now in the Unitary namespace. And the results unitary.spectrum.unitary_conjugate and unitary.spectrum.unitary_conjugate' are renamed to Unitary.spectrum_star_conjugate_left and Unitary.spectrum_star_conjugate_right to match the renaming convention in #30692.

Estimated changes

added theorem Unitary.coe_div
added theorem Unitary.coe_inv
added theorem Unitary.coe_map
added theorem Unitary.coe_map_star
added theorem Unitary.coe_neg
added theorem Unitary.coe_smul
added theorem Unitary.coe_star
added theorem Unitary.coe_zpow
added theorem Unitary.inv_mem
added def Unitary.map
added def Unitary.mapEquiv
added theorem Unitary.mapEquiv_refl
added theorem Unitary.mapEquiv_symm
added theorem Unitary.mapEquiv_trans
added theorem Unitary.map_comp
added theorem Unitary.map_id
added theorem Unitary.map_injective
added theorem Unitary.map_mem
added theorem Unitary.mem_iff
added theorem Unitary.mul_star_self
added theorem Unitary.smul_mem
added theorem Unitary.star_eq_inv'
added theorem Unitary.star_eq_inv
added theorem Unitary.star_mem
added theorem Unitary.star_mem_iff
added theorem Unitary.star_mul_self
added def Unitary.toUnits
deleted theorem unitary.coe_div
deleted theorem unitary.coe_inv
deleted theorem unitary.coe_map
deleted theorem unitary.coe_map_star
deleted theorem unitary.coe_mul_star_self
deleted theorem unitary.coe_neg
deleted theorem unitary.coe_smul
deleted theorem unitary.coe_star
deleted theorem unitary.coe_star_mul_self
deleted theorem unitary.coe_zpow
deleted theorem unitary.inv_mem
deleted theorem unitary.inv_mul_mem_iff
deleted def unitary.map
deleted def unitary.mapEquiv
deleted theorem unitary.mapEquiv_refl
deleted theorem unitary.mapEquiv_symm
deleted theorem unitary.mapEquiv_trans
deleted theorem unitary.map_comp
deleted theorem unitary.map_id
deleted theorem unitary.map_injective
deleted theorem unitary.map_mem
deleted theorem unitary.mem_iff
deleted theorem unitary.mul_inv_mem_iff
deleted theorem unitary.mul_star_self
deleted theorem unitary.smul_mem
deleted theorem unitary.smul_mem_of_mem
deleted theorem unitary.star_eq_inv'
deleted theorem unitary.star_eq_inv
deleted theorem unitary.star_mem
deleted theorem unitary.star_mem_iff
deleted theorem unitary.star_mul_self
deleted def unitary.toUnits
deleted theorem unitary.toUnits_comp_map
deleted theorem unitary.toUnits_injective
added theorem Unitary.joined
added theorem Unitary.norm_sub_eq
deleted theorem unitary.joined
deleted theorem unitary.norm_sub_eq
added theorem Unitary.inner_map_map
added theorem Unitary.norm_map
deleted theorem unitary.inner_map_map
deleted theorem unitary.norm_map