Commit 2022-05-02 19:32 c44091fc
View on Github →feat(data/zmod/basic): Generalize zmod.card (#13887)
This PR generalizes zmod.card from assuming [fact (0 < n)] to assuming [fintype (zmod n)].
Note that the latter was already part of the statement, but was previously deduced from the instance instance fintype : Π (n : ℕ) [fact (0 < n)], fintype (zmod n) on line 80.