Theorem MDifferentiable.exists_eq_const_of_compactSpace

Modification history

2026-03-06 14:49
Mathlib/Geometry/Manifold/Complex.lean
chore: golf using custom elaborators (#36235) …
Modified MDifferentiable.exists_eq_const_of_compactSpaceView on Github →
2023-06-27 14:29
Mathlib/Geometry/Manifold/Complex.lean
feat: port Geometry.Manifold.Complex (#5498)
Added MDifferentiable.exists_eq_const_of_compactSpaceView on Github →