Eric Ren (Jan 13 2025 at 20:38): Eric Ren (Jan 13 2025 at 20:38):Hi,
I'm trying to prove this toy lemma in cring, but I get an error when I try to use "^". I don't know why that's the case, since Ring seems to instantiate "^".
Here's my code and imports.
Screenshot 2025-01-13 122404.png
Screenshot 2025-01-13 123540.png
Mathias Fleury (Jan 14 2025 at 06:47):And then you obviously control-clicked on the multiplication symbol, searched for pow in the file, and found that the syntax was [^]
Mathias Fleury (Jan 14 2025 at 06:48):(As a side remark, give your code as text too. Screenshots are annoying.)
Eric Ren (Jan 14 2025 at 14:55):Oh, I'd actually tried that, but I must've had a second error, glanced at that error message, and not realized that it works. Sorry about that. Thanks.
Last updated: Feb 01 2025 at 20:19 UTC