Theorem new_name_mul

Modification history

2025-08-11 18:06
MathlibTest/DeprecateTo.lean
chore: reformat `to_additive` docstrings to use `docComment` syntax (#28066) …
Added new_name_mulView on Github →