Theorem unitary.coe_zpow

Modification history

2025-10-29 21:09
Mathlib/Algebra/Star/Unitary.lean
chore: move results from `unitary` namespace to `Unitary` (#30697) …
Deleted unitary.coe_zpowView on Github →
2023-01-19 07:45
Mathlib/Algebra/Star/Unitary.lean
chore: format `by` line breaks (#1523) …
Modified unitary.coe_zpowView on Github →
2023-01-09 16:13
Mathlib/Algebra/Star/Unitary.lean
feat: Port Algebra.Star.Unitary (#1436)
Added unitary.coe_zpowView on Github →