no goals
n' : Type u_2
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_1
inst✝ : CommRing R
u : Mˣ
n : ℕ
⊢ ↑(u ^ ↑n) = ↑u ^ ↑n
rw [_root_.zpow_coe_nat, zpow_ofNat, Units.val_pow_eq_pow_val]
no goals
n' : Type u_2
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_1
inst✝ : CommRing R
u : Mˣ
k : ℕ
⊢ ↑(u ^ -[k+1]) = ↑u ^ -[k+1]
rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv]