mul_right_iff — Mathlib

English

IsRelPrime of x with y·z is equivalent to IsRelPrime x with y and IsRelPrime x with z.

Русский

IsRelPrime(x, y·z) эквивалентно IsRelPrime(x,y) и IsRelPrime(x,z).

LaTeX

$$$\text{IsRelPrime}(x, y \cdot z) \iff \big( \text{IsRelPrime}(x,y) \land \text{IsRelPrime}(x,z) \big)$$$

Lean4

theorem mul_right_iff : IsRelPrime x (y * z) ↔ IsRelPrime x y ∧ IsRelPrime x z :=
  ⟨fun H ↦ ⟨H.of_mul_right_left, H.of_mul_right_right⟩, fun ⟨H1, H2⟩ ↦ H1.mul_right H2⟩

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