u : ℤˣ
⊢ natAbs 1 = 1
u : ℤˣ
⊢ natAbs ↑u * natAbs ↑u⁻¹ = 1
rw [← natAbs_mul, Units.mul_inv]
no goals
u : ℤˣ
⊢ natAbs 1 = 1
rfl
u : ℤˣ
⊢ natAbs 1 = 1
u : ℤˣ
⊢ natAbs ↑u⁻¹ * natAbs ↑u = 1
rw [← natAbs_mul, Units.inv_mul]
no goals
u : ℤˣ
⊢ natAbs 1 = 1
rfl