Commit 2025-08-25 05:08 0ab76acc

View on Github →

chore(Data/Int): add norm_cast attrs (#28888)

  • Add two norm_cast attributes.
  • Rename IsCoprime.nat_coprime to IsCoprime.natCoprime.
  • Rewrite 2 proofs to use mod_cast or induction.

Estimated changes

modified theorem IsCoprime.prod_left