natCast_factorial_of_lt — Mathlib

English

If (n−1)! is a unit in A, then for every m < n, m! is a unit in A.

Русский

Если (n−1)! является единицей в A, то для каждого m < n m! является единицей в A.

LaTeX

$$$ (n-1)! : A \text{ unit} \Rightarrow (m! : A) \text{ unit for all } m < n $$$

Lean4

theorem natCast_factorial_of_lt {n : ℕ} (hn_fac : IsUnit ((n - 1)! : A)) {m : ℕ} (hmn : m < n) : IsUnit (m ! : A) :=
  hn_fac.natCast_factorial_of_le <| le_sub_one_of_lt hmn

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