isClassified_of_normalize_isPrimitiveClassified

English

If the normalized triple h.normalize is primitive-classified, then h is classified.

Русский

Если нормализованная тройка h.normalize примитивно классифицирована, то исходная тройка классифицирована.

LaTeX

$$$h.normalize.IsPrimitiveClassified \Rightarrow h.IsClassified$$$

Lean4

theorem isClassified_of_normalize_isPrimitiveClassified (hc : h.normalize.IsPrimitiveClassified) : h.IsClassified :=
  by
  convert h.normalize.mul_isClassified (Int.gcd x y) (isClassified_of_isPrimitiveClassified h.normalize hc) <;>
    rw [Int.mul_ediv_cancel']
  · exact Int.gcd_dvd_left ..
  · exact Int.gcd_dvd_right ..
  · exact h.gcd_dvd

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