Theorem one_eq_one'''

Modification history

2025-05-14 19:14
MathlibTest/toAdditive.lean
feat(Tactic/ToAdditive): check that existing additive declaration matches up (#24401) …
Added one_eq_one'''View on Github →