mul_left_iff — Mathlib

English

IsRelPrime of x*y with z is equivalent to x relatively prime to z and y relatively prime to z.

Русский

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

LaTeX

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

Lean4

theorem mul_left_iff : IsRelPrime (x * y) z ↔ IsRelPrime x z ∧ IsRelPrime y z :=
  ⟨fun H ↦ ⟨H.of_mul_left_left, H.of_mul_left_right⟩, fun ⟨H1, H2⟩ ↦ H1.mul_left H2⟩

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