divNat_mul_divNat — Mathlib

English

The product of divNat representations equals the divNat of the product of numerators and denominators: divNat(n1,d1) · divNat(n2,d2) = divNat(n1·n2, d1·d2).

Русский

Произведение представлений divNat равно divNat от произведения числителей и знаменателей.

LaTeX

$$$ \operatorname{divNat}(n_1,d_1) \cdot \operatorname{divNat}(n_2,d_2) = \operatorname{divNat}(n_1 n_2, d_1 d_2) $$$

Lean4

theorem divNat_mul_divNat (n₁ n₂ : ℕ) {d₁ d₂} : divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂) := by ext;
  push_cast; exact Rat.divInt_mul_divInt _ _

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