Invertibility of factorials

This file contains lemmas providing sufficient conditions for the cast of n! to a (semi)ring A to be a unit.

theorem IsUnit.natCast_factorial_of_le {A : Type u_1} [Semiring A] {n : ℕ} (hn_fac : IsUnit ↑n.factorial) {m : ℕ} (hmn : m ≤ n) : IsUnit ↑m.factorial

theorem IsUnit.natCast_factorial_of_lt {A : Type u_1} [Semiring A] {n : ℕ} (hn_fac : IsUnit ↑(n - 1).factorial) {m : ℕ} (hmn : m < n) : IsUnit ↑m.factorial

theorem IsUnit.natCast_factorial_of_algebra {A : Type u_1} [Semiring A] (K : Type u_2) [Semifield K] [CharZero K] [Algebra K A] (n : ℕ) : IsUnit ↑n.factorial

If A is an algebra over a characteristic-zero (semi)field, then n! is a unit.

theorem IsUnit.natCast_factorial_iff_of_charP {A : Type u_1} [Ring A] (p : ℕ) [Fact (Nat.Prime p)] [CharP A p] {n : ℕ} : IsUnit ↑n.factorial ↔ n < p

theorem IsUnit.natCast_of_isNilpotent_of_coprime {A : Type u_1} [CommRing A] {n p : ℕ} (hp : IsNilpotent ↑p) (h : p.Coprime n) : IsUnit ↑n

theorem IsUnit.natCast_factorial_of_isNilpotent {A : Type u_1} [CommRing A] {n p : ℕ} (hp : IsNilpotent ↑p) [Fact (Nat.Prime p)] (h : n < p) : IsUnit ↑n.factorial

theorem Nat.castChoose_eq {A : Type u_1} [CommSemiring A] {m : ℕ} {k : ℕ × ℕ} (hm : IsUnit ↑m.factorial) (hk : k ∈ Finset.antidiagonal m) : ↑(m.choose k.1) = ↑m.factorial * Ring.inverse ↑k.1.factorial * Ring.inverse ↑k.2.factorial