Commit 2025-02-17 17:27 dcaa8e65
View on Github →chore(Algebra): upstream Int.cast_mul_eq_zsmul_cast (#21993)
This lemma lives in a file about the ordered ring structure on Int but can happily live without knowing about orders, next to Int.cast_mul which it is a slight generalization of. Spotted while looking at grey imports for Algebra.ModEq in Algebra.CharP.Defs.