Theorem: norm_intCast (FltRegular/ReadyForMathlib/PowerBasis.lean)

State before:
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 ℚ) ↑n = ↑n ^ finrank ℚ K
Tactic:
rw [← eq_intCast (algebraMap ℤ (𝓞 K)) n, IsScalarTower.algebraMap_apply ℤ (𝓞 ℚ) (𝓞 K)]
State after:
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

State before:
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
Tactic:
simp only [norm_algebraMap, algebraMap_int_eq, Int.coe_castRingHom, eq_intCast, Int.cast_pow]
State after:
no goals