Mathlib Changelog
v4
Changelog
About
Github
Theorem
IsContDiffImplicitAt.implicitFunctionData_rightFun_apply
Modification history
2026-01-08 19:45
Mathlib/Analysis/Calculus/ImplicitContDiff.lean
feat: uniqueness API for implicit function of `IsContDiffImplicitAt` (#31988)
Added
IsContDiffImplicitAt.implicitFunctionData_rightFun_apply
View on Github →