isCoprime_self — Mathlib

English

For any x in a commutative semiring, x is coprime with itself exactly when x is a unit.

Русский

Для любого x в коммутативном полупринднике x взаимно просто с самим собой тогда и только тогда, когда x является единицей.

LaTeX

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

Lean4

theorem isCoprime_self : IsCoprime x x ↔ IsUnit x :=
  ⟨fun ⟨a, b, h⟩ => isUnit_of_mul_eq_one x (a + b) <| by rwa [mul_comm, add_mul], fun h =>
    let ⟨b, hb⟩ := isUnit_iff_exists_inv'.1 h
    ⟨b, 0, by rwa [zero_mul, add_zero]⟩⟩

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