divisibleByIntOfCharZero — Mathlib

English

In a division ring of characteristic zero, integers act by division: div q n = q / n, and this defines DivisibleBy 𝕜 ℤ.

Русский

В делительном кольце характеристики ноль целые числа действуют через деление: div q n = q / n, что задаёт делимость по ℤ.

LaTeX

$$$\text{DivisibleBy } 𝕜 \mathbb{Z}$, with\div q n = q / n,\; div_zero = 0,\; div_cancel \\text{(for nonzero } n\text{)}$$

Lean4

instance (priority := 100) divisibleByIntOfCharZero {𝕜} [DivisionRing 𝕜] [CharZero 𝕜] : DivisibleBy 𝕜 ℤ
    where
  div q n := q / n
  div_zero q := by simp
  div_cancel {n} q hn := by rw [zsmul_eq_mul, (Int.cast_commute n _).eq, div_mul_cancel₀ q (Int.cast_ne_zero.mpr hn)]

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