Zulip Chat Archive
Stream: mathlib4
Topic: naming ext lemmas
Kevin Buzzard (Nov 26 2022 at 20:08):
Making a structure. Can I use the ext tag and specify the names of the lemmas? I'm in an unfortunate situation where applying ext clobbers a later declaration which is not the same.
Kevin Buzzard (Nov 26 2022 at 20:10):
Oh I can just #align my way out of this particular problem.
Last updated: Dec 20 2023 at 11:08 UTC