feat(Mathlib/Data/Nat/Factorial/NatCast): add IsUnit lemmas (#22237)

Co-authored-by: AntoineChambert-Loir <[email protected]>
Co'authored-by: Eric Wieser [eric-wieser](https://github.com/eric-wieser)



Co-authored-by: Eric Wieser <[email protected]>

Mathlib.lean

@@ -3054,6 +3054,7 @@ import Mathlib.Data.Nat.Factorial.Basic
 import Mathlib.Data.Nat.Factorial.BigOperators
 import Mathlib.Data.Nat.Factorial.Cast
 import Mathlib.Data.Nat.Factorial.DoubleFactorial
+import Mathlib.Data.Nat.Factorial.NatCast
 import Mathlib.Data.Nat.Factorial.SuperFactorial
 import Mathlib.Data.Nat.Factorization.Basic
 import Mathlib.Data.Nat.Factorization.Defs

Mathlib/Data/Nat/Factorial/NatCast.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2025 Antoine Chambert-Loir, María Inés de Frutos-Fernández. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández
+-/
+
+import Mathlib.Algebra.Algebra.Defs
+import Mathlib.Algebra.CharP.Invertible
+import Mathlib.Algebra.Order.Group.Nat
+import Mathlib.Data.Nat.Factorial.Basic
+
+/-!
+# Invertibility of factorials
+
+This file contains lemmas providing sufficient conditions for the cast of `n!` to a (semi)ring `A`
+to be a unit.
+
+-/
+
+namespace IsUnit
+
+open Nat
+section Semiring
+
+variable {A : Type*} [Semiring A]
+
+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
+
+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
+
+/-- If `A` is an algebra over a characteristic-zero (semi)field, then `n!` is a unit. -/
+theorem natCast_factorial_of_algebra (K : Type*) [Semifield K] [CharZero K] [Algebra K A] (n : ℕ) :
+    IsUnit (n ! : A) := by
+  suffices IsUnit (n ! : K) by
+    simpa using this.map (algebraMap K A)
+  simp [isUnit_iff_ne_zero, n.factorial_ne_zero]
+
+end Semiring
+
+section CharP
+
+variable {A : Type*} [Ring A] (p : ℕ) [Fact (Nat.Prime p)] [CharP A p]
+
+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⟩⟩
+
+end CharP
+
+end IsUnit