natCast_factorial_of_le — Mathlib

English

In any semiring S, if n! is a unit, then m! is a unit for every m ≤ n.

Русский

В любом полукольце S, если n! является единицей, то для каждого m ≤ n также m! является единицей.

LaTeX

$$$ (n! : S) \text{ is a unit } \Rightarrow (m! : S) \text{ is a unit for all } m \le n $$$

Lean4

theorem natCast_factorial_of_le {n : ℕ} (hn_fac : IsUnit (n ! : A)) {m : ℕ} (hmn : m ≤ n) : IsUnit (m ! : A) :=
  by
  obtain ⟨k, rfl⟩ := exists_add_of_le hmn
  clear hmn
  induction k generalizing m with
  | zero => simpa using hn_fac
  | succ k ih =>
    rw [← add_assoc, add_right_comm] at hn_fac
    have := ih hn_fac
    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff] at this
    exact this.2

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