Zulip Chat Archive
Stream: lean4
Topic: rw [← add_smul] fails to find pattern in Vector Space World
Notification Bot (Dec 13 2025 at 09:30):
This topic was moved to #new members > rw [← add_smul] fails to find pattern in Vector Space World by Patrick Massot.
Last updated: Dec 20 2025 at 21:32 UTC