cast_div_charZero — Mathlib

English

For a DivisionSemiring K of characteristic zero, if n divides m, then the cast of m/n equals m/n in K.

Русский

Для DivisionSemiring K характеристики ноль, если n делит m, то приведение m/n равно m/n в K.

LaTeX

$$$ \uparrow (m / n) = m / n \quad\text{if } n \mid m \text{ and } [CharZero K]$$$

Lean4

@[simp, norm_cast]
theorem cast_div_charZero (hnm : n ∣ m) : (↑(m / n) : K) = m / n := by obtain rfl | hn := eq_or_ne n 0 <;> simp [*]

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