a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
n0 : n ≠ 0
⊢ n /. ↑d * (n /. ↑d)⁻¹ = 1
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
⊢ n /. ↑d * (n /. ↑d)⁻¹ = 1
have n0 : n ≠ 0 := mt (by rintro rfl; simp) a0
no goals
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
n0 : n ≠ 0
⊢ n /. ↑d * (n /. ↑d)⁻¹ = 1
simpa [h, n0, mul_comm] using @divInt_mul_right 1 1 (n * d) (by simp [h, n0])
a b c : ℚ
d : ℕ
h : d ≠ 0
a0 : 0 /. ↑d ≠ 0
⊢ 0 /. ↑d = 0
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
⊢ n = 0 → n /. ↑d = 0
rintro rfl
no goals
a b c : ℚ
d : ℕ
h : d ≠ 0
a0 : 0 /. ↑d ≠ 0
⊢ 0 /. ↑d = 0
simp
no goals
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
n0 : n ≠ 0
⊢ n * ↑d ≠ 0
simp [h, n0]