Mathlib Changelog
v4
Changelog
About
Github
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 →