natCast_factorial_of_isNilpotent — Mathlib

English

If p is nilpotent and p is prime, then for n < p, n! is a unit in A.

Русский

Если p нильпотент и простое, то для n < p факториал n! является единицей в A.

LaTeX

$$$ [Fact\ p.Prime] \; (n < p) \Rightarrow (n! : A) \text{ is a unit}$$$

Lean4

theorem natCast_factorial_of_isNilpotent [Fact p.Prime] (h : n < p) : IsUnit (n ! : A) := by
  induction n with
  | zero => simp
  | succ n ih =>
    simp only [factorial_succ, cast_mul, IsUnit.mul_iff]
    refine ⟨.natCast_of_isNilpotent_of_coprime hp ?_, ih (by cutsat)⟩
    rw [Nat.Prime.coprime_iff_not_dvd Fact.out]
    exact Nat.not_dvd_of_pos_of_lt (by cutsat) h

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