natCast_of_isNilpotent_of_coprime

English

If p is nilpotent in a commutative ring A and p is coprime to n, then n is a unit in A.

Русский

Если p является нильпотентом в коммутативном кольце A и p взаимно прост с n, то n является единицей в A.

LaTeX

$$$ \text{IsNilpotent}(p).cast \Rightarrow (\gcd(p,n)=1) \Rightarrow (n : A) \text{ is a unit}$$$

Lean4

theorem natCast_of_isNilpotent_of_coprime (h : p.Coprime n) : IsUnit (n : A) :=
  by
  obtain ⟨m, hm⟩ := hp
  suffices ∃ a b : A, p ^ m * a + n * b = 1 by
    obtain ⟨a, b, h⟩ := this
    apply isUnit_of_mul_eq_one (n : A) b
    simpa [hm] using h
  refine ⟨(p ^ m).gcdA n, (p ^ m).gcdB n, ?_⟩
  norm_cast
  rw [← Nat.cast_one, ← Int.cast_natCast 1, ← (h.pow_left m).gcd_eq_one, Nat.gcd_eq_gcd_ab]

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