Commits on Apr 4, 2022

1. feat(ring_theory/unique_factorization_domain): alternative specificat… …

   …ion for `count (normalized_factors x)`
   
   `count_normalized_factors_eq` specifies the number of times an irreducible
   factor `p` appears in `normalized_factors x`, namely the number of times it
   divides `x`. This is often easier to work with than going through `multiplicity`
   since this way we avoid coercing to `enat`

   

   Vierkantor committed Apr 4, 2022
   Configuration menu

   • View commit details
   • Copy full SHA for 301a3d2
   • Browse repository at this point

   Copy the full SHA

   301a3d2 View commit details

   Browse the repository at this point in the history