Theorem unitary.coe_smul

Modification history

2025-10-29 21:09
Mathlib/Algebra/Star/Unitary.lean
chore: move results from `unitary` namespace to `Unitary` (#30697) …
Deleted unitary.coe_smulView on Github →
2025-08-18 20:42
Mathlib/Algebra/Star/Unitary.lean
feat: lift star-preserving actions to actions between unitary groups (#28309)
Added unitary.coe_smulView on Github →