cast_div_div_div_cancel_right — Mathlib

English

If d divides both n and m, then (m/d) cast divided by (n/d) cast equals m cast divided by n in K.

Русский

Если d делит и n, и m, то (m/d)^{\uparrow} /(n/d)^{\uparrow} = m^{\uparrow} / n в K.

LaTeX

$$$ (\uparrow (m / d) : K) / (\uparrow (n / d) : K) = (m : K) / n $ при $ d \mid n$ и $ d \mid m$$$

Lean4

theorem cast_div_div_div_cancel_right (hn : d ∣ n) (hm : d ∣ m) : (↑(m / d) : K) / (↑(n / d) : K) = (m : K) / n :=
  by
  rcases eq_or_ne d 0 with (rfl | hd); · simp [Nat.zero_dvd.1 hm]
  replace hd : (d : K) ≠ 0 := by norm_cast
  rw [cast_div hm, cast_div hn, div_div_div_cancel_right₀ hd] <;> exact hd

Похожие утверждения