Zulip Chat Archive
Stream: general
Topic: how does `norm_num` handle smul?
Eric Wieser (Jan 11 2023 at 11:55):
Looking through the src#tactic.interactive.norm_num source, I was able to find plenty of mentions of pow, yet none of smul.
How then is it able to prove example {α} [ring α] : (2 • 3 : α) = 6 := by norm_num?
Eric Wieser (Jan 11 2023 at 11:57):
Oh, I didn't realize that docs#nsmul_eq_mul was a simp lemma, nevermind
Last updated: May 02 2025 at 03:31 UTC