exists_reduced_factors' — Mathlib

English

A symmetric reformulation: from a,b with hb ≠ 0, there exist a', b', c' with IsRelPrime a' b' and c' a' = a and c' b' = b.

Русский

Симметричная формулировка: из a,b с hb ≠ 0 существуют a', b', c' с взаимно простыми a', b' и c' a' = a, c' b' = b.

LaTeX

$$$a,b: R; hb \neq 0 \Rightarrow \exists a',b',c', \mathrm{IsRelPrime}(a',b') \land c'a' = a \land c'b' = b.$$$

Lean4

theorem exists_reduced_factors' (a b : R) (hb : b ≠ 0) : ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b :=
  let ⟨b', a', c', no_factor, hb, ha⟩ := exists_reduced_factors b hb a
  ⟨a', b', c', fun _ hpb hpa => no_factor hpa hpb, ha, hb⟩

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