Commit 2024-11-01 03:45 7a323ac4

View on Github →

refactor(SetTheory/Ordinal/Principal): fix bad names (#17842) This PR performs the following renames:

  • principal_add_isLimit → isLimit_of_principal_add
  • principal_mul_isLimit → isLimit_of_principal_mul
  • opow_principal_add_of_principal_add → principal_add_opow_of_principal_add
  • mul_principal_add_is_principal_add → principal_add_mul_of_principal_add

Estimated changes