fdiv_fdiv_eq_fdiv_mul — Mathlib

English

For m ∈ ℤ and n,k ∈ ℤ with n ≥ 0 and k ≥ 0, (m.fdiv n).fdiv k = m.fdiv(n·k).

Русский

Для m ∈ ℤ и n,k ∈ ℤ с n ≥ 0 и k ≥ 0 выполняется (m.fdiv n).fdiv k = m.fdiv(n·k).

LaTeX

$$$ (m \mathrm{fdiv} n) \mathrm{fdiv} k = m \mathrm{fdiv}(n k) $$$

Lean4

theorem fdiv_fdiv_eq_fdiv_mul (m : Int) {n k : Int} (hn : 0 ≤ n) (hk : 0 ≤ k) : (m.fdiv n).fdiv k = m.fdiv (n * k) := by
  rw [Int.fdiv_eq_ediv_of_nonneg _ hn, Int.fdiv_eq_ediv_of_nonneg _ hk,
    Int.fdiv_eq_ediv_of_nonneg _ (Int.mul_nonneg hn hk), ediv_ediv hn]

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