iterateFrobenius_inj — Mathlib

English

Let R be a commutative reduced ring and p a natural number with ExpChar R p. Then the iterated Frobenius endomorphism is injective for every n.

Русский

Пусть R — коммутативное редуцируемое кольцо, и p — натуральное число с ExpChar R p. Тогда для каждого n итеративный Фробениусов переход вводится инъективно.

LaTeX

$$$\\text{injective}(\\operatorname{iterateFrobenius} \\, R \\, p \\, n)$$$

Lean4

theorem iterateFrobenius_inj : Function.Injective (iterateFrobenius R p n) := fun x y H ↦
  by
  rw [← sub_eq_zero] at H ⊢
  simp_rw [iterateFrobenius_def, ← sub_pow_expChar_pow] at H
  exact IsReduced.eq_zero _ ⟨_, H⟩

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