Zulip Chat Archive
Stream: mathlib4
Topic: Notation for dilation
Yury G. Kudryashov (Jul 07 2023 at 03:21):
I'm adding DilationEquiv and I want to introduce notation →ᵈ and ≃ᵈ for docs#Dilation and DilationEquiv, respectively. Any objections?
Yury G. Kudryashov (Jul 07 2023 at 13:07):
Last updated: Dec 20 2023 at 11:08 UTC