Commit 2024-07-22 11:41 d25a5079

View on Github →

chore: split off Defs and Induction from Nat/Factorization/Basic (#14960) Nat/Factorization/Basic has 900 lines and 5 imports. This PR reduces size and number of imported files in several downstream files by importing the minimal newly created Nat/Factorization/Defs or Nat/Factorization/Induction

Estimated changes

deleted def Nat.factorization
deleted theorem Nat.factorization_def
deleted theorem Nat.factorization_inj
deleted theorem Nat.factorization_mul
deleted theorem Nat.factorization_one
deleted theorem Nat.factorization_pow
deleted theorem Nat.factorization_prod
deleted theorem Nat.factorization_zero
deleted theorem Nat.ord_proj_dvd
deleted def Nat.recOnMul
deleted def Nat.recOnPrimePow
deleted theorem Nat.support_factorization
added theorem Nat.factorization_def
added theorem Nat.factorization_inj
added theorem Nat.factorization_mul
added theorem Nat.factorization_one
added theorem Nat.factorization_pow
added theorem Nat.factorization_prod
added theorem Nat.factorization_zero
added theorem Nat.ord_proj_dvd
added def Nat.recOnMul