Documentation

Mathlib.Data.Nat.Choose.Cast

Cast of binomial coefficients #

This file allows calculating the binomial coefficient a.choose b as an element of a division ring of characteristic 0.