Commit 2024-11-03 19:16 0edf93d8

View on Github →

chore(Nat.Factorization): rename ord_proj/compl -> ordProj/Compl (#18191) Since both ord_proj and ord_compl expand to data (a Nat), they should be camelCased. This PR renames them to ordProj and ordCompl respectively and deprecates the old names in declarations.

Estimated changes

added theorem Nat.coprime_ordCompl
deleted theorem Nat.coprime_ord_compl
added theorem Nat.dvd_ordProj_of_dvd
deleted theorem Nat.dvd_ord_proj_of_dvd
added theorem Nat.not_dvd_ordCompl
deleted theorem Nat.not_dvd_ord_compl
added theorem Nat.ordCompl_dvd
added theorem Nat.ordCompl_le
added theorem Nat.ordCompl_mul
added theorem Nat.ordCompl_pos
added theorem Nat.ordProj_le
added theorem Nat.ordProj_mul
added theorem Nat.ordProj_pos
deleted theorem Nat.ord_compl_dvd
deleted theorem Nat.ord_compl_le
deleted theorem Nat.ord_compl_mul
deleted theorem Nat.ord_compl_pos
deleted theorem Nat.ord_proj_le
deleted theorem Nat.ord_proj_mul
deleted theorem Nat.ord_proj_of_not_prime
deleted theorem Nat.ord_proj_pos
added theorem Nat.ordProj_dvd
deleted theorem Nat.ord_proj_dvd