Is there a way to use ' in notation?

Stream: lean4

[Daniel Weber]

I want to define differential rings and fields, and I'd like to use the notation a' for the derivative of a. Is there a way to do that? postfix:75 "'" => Differential.deriv fails.
If not, what would be the closest alternative? Perhaps some unicode character?

[Yaël Dillies]

Actually I believe some people already have work on differential rings and the notation they use is ∂ a

[Daniel Weber]

I see. Do you have any idea where I could find it? I didn't see anything in Mathlib

[Daniel Weber]

I found docs#Derivation, and https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Differential.20Rings and https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/antiderivative, but they're quite old

[Kyle Miller]

' probably couldn't work since it's used for character literals like 'a', but you could use a unicode character, like the prime symbol:

postfix:75 "′" => Differential.deriv

[Daniel Weber]

Is there anything I could change in VSCode to get \' to give prime?

[Kevin Buzzard]

You could make a PR to the file https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json

I am a bit unclear about how it will affect entries such as "'A": "Á",

[Yaël Dillies]

Daniel Weber said:

I see. Do you have any idea where I could find it? I didn't see anything in Mathlib

I'm trying to remember whether "some people" includes me