refactor(Peripheral): use native power norm

Author: texra-ai

TNLean/Channel/Peripheral/ClosureFixedPoint.lean

@@ -174,7 +174,8 @@ theorem peripheralEigenvalues_pow_mem_of_irreducible_unital_of_adjoint_fixedPoin
     refine Module.End.hasEigenvalue_of_hasEigenvector (x := X ^ n) ?_
     refine (Module.End.hasEigenvector_iff.mpr ?_)
     exact ⟨(Module.End.mem_eigenspace_iff).2 hpow_transfer, hXpow_ne⟩
-  refine ⟨hEigPow_transfer, norm_pow_eq_one_of_norm_eq_one hμ_norm n⟩
+  refine ⟨hEigPow_transfer, ?_⟩
+  simp [norm_pow, hμ_norm]
 
 /-- For irreducible unital Kraus maps with a positive definite adjoint fixed point,
 all peripheral eigenvalues are roots of unity.

TNLean/Channel/Peripheral/IrreducibleChannel.lean

@@ -175,7 +175,8 @@ theorem peripheral_isRootOfUnity_of_irreducible_channel [NeZero D]
   have hμp_eig : Module.End.HasEigenvalue
       ((MPSTensor.transferMap (d := r) (D := D) K) ^ p) (μ ^ p) := by
     simpa [hE_eq] using hμ_eig.pow p
-  have hμp_norm : ‖μ ^ p‖ = 1 := norm_pow_eq_one_of_norm_eq_one hμ_norm p
+  have hμp_norm : ‖μ ^ p‖ = 1 := by
+    simp [norm_pow, hμ_norm]
   exact ⟨p, hp_pos, hPrimP.unique_peripheral (μ ^ p) hμp_eig hμp_norm⟩
 
 /-- Channel-level formulation for `compl_eigenvalue_norm_lt_one_of_primitive`.

TNLean/Channel/Peripheral/Spectrum.lean

@@ -79,10 +79,6 @@ theorem one_mem_peripheralEigenvalues
     (1 : ℂ) ∈ peripheralEigenvalues E :=
   ⟨hasEigenvalue_of_eigenvector_eq E 1 ρ (by simp [hfix]) hne, by simp⟩
 
-/-- Powers of a unit-norm complex number have norm 1. -/
-theorem norm_pow_eq_one_of_norm_eq_one {μ : ℂ} (hμ : ‖μ‖ = 1) (n : ℕ) :
-    ‖μ ^ n‖ = 1 := by rw [norm_pow, hμ, one_pow]
-
 /-- In finite dimensions, the peripheral eigenvalue set is finite. -/
 theorem peripheralEigenvalues_finite
     {V : Type*} [AddCommGroup V] [Module ℂ V]

TNLean/Wielandt/Primitivity/ImpliesStronglyIrreducibleAux.lean

@@ -615,7 +615,8 @@ theorem isPeripherallyPrimitive_of_isPrimitivePaper [NeZero D]
         ((Module.End.hasEigenvector_iff.mpr
           ⟨Module.End.mem_eigenspace_iff.mpr hEigP, hX_ne⟩))
     -- ‖μ^p‖ = 1
-    have hμp_norm : ‖μ ^ p‖ = 1 := norm_pow_eq_one_of_norm_eq_one hμ_norm p
+    have hμp_norm : ‖μ ^ p‖ = 1 := by
+      simp [norm_pow, hμ_norm]
     -- By IsPrimitive (E^p): μ^p = 1
     have hμp_eq : μ ^ p = 1 := hPrimP.unique_peripheral (μ ^ p) hμp_eig hμp_norm
     -- If μ ≠ 1, get contradiction via Part 13