Commit 2025-03-29 19:12 cd5ac5a1

refactor: protect map_mul lemmas (#23403) The lemmas map_mul and map_one are among the most widely used simp lemmas; but there are a number of slightly different lemmas with the same names in various namespaces, meaning the root-namespace lemmas need to be called with _root_ when these namespaces are open. This PR adds the protected flag to the following lemmas:

• FractionalIdeal.map_mul
• FractionalIdeal.map_one
• FractionalIdeal.map_div
• FractionalIdeal.map_inv
• Matrix.map_mul
• Matrix.map_one
• ENat.map_one
• Ideal.map_mul
• CliffordAlgebra.reverse.map_mul
• CliffordAlgebra.reverse.map_one
• PiTensorProduct.map_mul
• PiTensorProduct.map_one,
• Valuation.map_mul
• Valuation.map_one which allows removing the _root_ prefix from > 150 instances of _root_.map_mul and _root_.map_one. Analogous fixes for additive versions (map_add, map_zero, etc) will be pursued in a subsequent PR.