isPrimitiveClassified_of_coprime_of_zero_left

English

If x = 0 and gcd x y = 1, then h.IsPrimitiveClassified.

Русский

Если x = 0 и gcd(x,y) = 1, то h примитивно классифицирована.

LaTeX

$$(x = 0 \land gcd(x,y) = 1) \Rightarrow h.IsPrimitiveClassified$$

Lean4

theorem isPrimitiveClassified_of_coprime_of_zero_left (hc : Int.gcd x y = 1) (hx : x = 0) : h.IsPrimitiveClassified :=
  by
  subst x
  change Nat.gcd 0 (Int.natAbs y) = 1 at hc
  rw [Nat.gcd_zero_left (Int.natAbs y)] at hc
  rcases Int.natAbs_eq y with hy | hy
  · use 1, 0
    rw [hy, hc, Int.gcd_zero_right]
    decide
  · use 0, 1
    rw [hy, hc, Int.gcd_zero_left]
    decide

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