simp only [norm_algebraMap, algebraMap_int_eq, Int.coe_castRingHom, eq_intCast, Int.cast_pow]
K✝ : Type ?u.45394
inst✝³ : Field K✝
pb : PowerBasis ℤ (𝓞 K✝)
inst✝² : NumberField K✝
hpr : _root_.Prime ((norm ℚ) pb.gen)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℤ
⊢ (norm ℚ) ((algebraMap (𝓞 ℚ) (𝓞 K)) ((algebraMap ℤ (𝓞 ℚ)) n)) = ↑n ^ finrank ℚ K
no goals