mathlib

0ccc1573 - feat(data/nat/fact, analysis/specific_limits): rename nat.fact, add few lemmas about its behaviour along at_top (#4309)

feat(data/nat/fact, analysis/specific_limits): rename nat.fact, add few lemmas about its behaviour along at_top (#4309) Main content : - Rename `nat.fact` to `nat.factorial`, and add notation `n!` in locale `factorial`. This fixes #2786 - Generalize `prod_inv_distrib` to `comm_group_with_zero` *without any nonzero assumptions* - `factorial_tendsto_at_top` : n! --> infinity as n--> infinity - `tendsto_factorial_div_pow_self_at_top` : n!/(n^n) --> 0 as n --> infinity