mathlib3
879155bf - feat(*): replace fact(0 < t) with ne_zero (#16145)

Commit
3 years ago
feat(*): replace fact(0 < t) with ne_zero (#16145) This has almost fully made things easier, whilst also being easier on the typeclass system (`fact` can cause many slowdowns). It also allows us to make many things that were not instances before into instances. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Author
Parents
Loading