Commit 2024-01-08 12:05 006e9a36
View on Github →chore: Move a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m (#9505)
Those lemmas were very recently added in #9397. Also make them iffs and golf.
Part of #9411
chore: Move a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m (#9505)
Those lemmas were very recently added in #9397. Also make them iffs and golf.
Part of #9411