Theorem Nat.castChoose_eq

Modification history

2025-09-05 17:21
Mathlib/Data/Nat/Factorial/NatCast.lean
feat(RingTheory/DividedPowers/RatAlgebra): add definitions (#22322) …
Added Nat.castChoose_eqView on Github →