isCoprime_zero_left — Mathlib

English

IsCoprime(0, x) holds if and only if x is a unit.

Русский

IsCoprime(0, x) выполняется тогда, когда x является единицей.

LaTeX

$$$IsCoprime(0,x) \iff IsUnit(x)$$$

Lean4

theorem isCoprime_zero_left : IsCoprime 0 x ↔ IsUnit x :=
  ⟨fun ⟨a, b, H⟩ => isUnit_of_mul_eq_one x b <| by rwa [mul_zero, zero_add, mul_comm] at H, fun H =>
    let ⟨b, hb⟩ := isUnit_iff_exists_inv'.1 H
    ⟨1, b, by rwa [one_mul, zero_add]⟩⟩

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