Commit 2022-02-14 20:17 263833cf
View on Github →feat(data/nat/factorization): add le_of_mem_factorization (#12032)
le_of_mem_factors: every factor of n is ≤ n
le_of_mem_factorization: everything in n.factorization.support is ≤ n
feat(data/nat/factorization): add le_of_mem_factorization (#12032)
le_of_mem_factors: every factor of n is ≤ n
le_of_mem_factorization: everything in n.factorization.support is ≤ n