ne_zero_or_ne_zero_of_nat_coprime

English

For A a nontrivial commutative ring, if a and b are coprime naturals, then (a : A) ≠ 0 or (b : A) ≠ 0.

Русский

Для ненулевого коммутативного кольца A, если a и b — взаимно простые натуральные числа, то их образы в A не оба нулевые.

LaTeX

$$($(a: A) \neq 0) \lor (b: A) \neq 0)$$

Lean4

theorem ne_zero_or_ne_zero_of_nat_coprime {A : Type u} [CommRing A] [Nontrivial A] {a b : ℕ} (h : Nat.Coprime a b) :
    (a : A) ≠ 0 ∨ (b : A) ≠ 0 :=
  IsCoprime.ne_zero_or_ne_zero (R := A) <| by
    simpa only [map_natCast] using IsCoprime.map (Nat.Coprime.isCoprime h) (Int.castRingHom A)

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