natCast_factorial_iff_of_charP — Mathlib

English

In a ring of characteristic p, with p prime, IsUnit(n! in A) iff n < p.

Русский

В кольце характеристика p, где p–слово простое, IsUnit(n! in A) эквивалентно n < p.

LaTeX

$$$ \text{IsUnit}(n! : A) \iff n < p $$$

Lean4

theorem natCast_factorial_iff_of_charP {n : ℕ} : IsUnit (n ! : A) ↔ n < p :=
  by
  have hp : p.Prime := Fact.out
  induction n with
  | zero => simp [hp.pos]
  | succ n ih =>
    -- TODO: why is `.symm.symm` needed here!?

    rw [factorial_succ, cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff, ih.symm.symm, ← Nat.add_one_le_iff,
      CharP.isUnit_natCast_iff hp]
    exact
      ⟨fun ⟨h1, h2⟩ ↦ lt_of_le_of_ne h2 (mt (· ▸ dvd_rfl) h1), fun h ↦ ⟨not_dvd_of_pos_of_lt (Nat.succ_pos _) h, h.le⟩⟩

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