cast_div — Mathlib

English

In a DivisionSemiring K, if n divides m and n ≠ 0 in K, then the cast of m/n equals m/n in K.

Русский

В DivisionSemiring K, если n делит m и n ≠ 0 в K, то приведение m/n равно m/n в K.

LaTeX

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

Lean4

@[simp]
theorem cast_div (hnm : n ∣ m) (hn : (n : K) ≠ 0) : (↑(m / n) : K) = m / n :=
  by
  obtain ⟨k, rfl⟩ := hnm
  have : n ≠ 0 := by rintro rfl; simp at hn
  rw [Nat.mul_div_cancel_left _ <| zero_lt_of_ne_zero this, mul_comm n, cast_mul, mul_div_cancel_right₀ _ hn]

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