feat: add Algebra.norm_zpow (leanprover-community#40238)

We generalize `Algebra.norm_inv` from fields to division rings and we add `Algebra.norm_zpow`.

From flt-regular.

Author: riccardobrasca

Mathlib/RingTheory/Norm/Basic.lean

@@ -127,12 +127,21 @@ theorem norm_ne_zero_iff_of_basis [IsDomain R] [IsDomain S] (b : Basis ι R S) {
     Algebra.norm R x ≠ 0 ↔ x ≠ 0 :=
   not_iff_not.mpr (norm_eq_zero_iff_of_basis b)
 
-theorem norm_inv [Module.Finite K L] (x : L) : Algebra.norm K x⁻¹ = (Algebra.norm K x)⁻¹ := by
+end EqZeroIff
+
+section DivisionRing
+
+variable {L : Type*} [DivisionRing L] [Algebra K L] [Module.Finite K L]
+
+theorem norm_inv (x : L) : Algebra.norm K x⁻¹ = (Algebra.norm K x)⁻¹ := by
   by_cases hx : x = 0
   · simp [hx]
   exact mul_left_injective₀ (norm_ne_zero_iff.mpr hx) (by simp [hx, ← map_mul])
 
-end EqZeroIff
+theorem norm_zpow (x : L) (n : ℤ) : Algebra.norm K (x ^ n) = Algebra.norm K x ^ n :=
+  map_zpow' _ norm_inv _ _
+
+end DivisionRing
 
 open IntermediateField