Commit 2025-06-27 05:04 501992c1
View on Github →feat: behavior of unique differentiablity under field extension (#26429)
If s is a domain of unique differentiability for a field k, then it is also a domain of unique differentiability for larger fields.
This PR provides material required to implement a reviewer's suggestion in https://github.com/leanprover-community/mathlib4/pull/26353