Monomials up to a unit on a real manifold, from Mathlib's definitions alone

IsMonomialAt n g p: near the point p of an n-dimensional real manifold, in the coordinates of the chart at p, the function g is a monomial times an analytic function that does not vanish at p. It is defined from Mathlib's charts (extChartAt) and analytic functions on manifolds (ContMDiffAt of order ω), in a module that imports Mathlib only. The challenge file Challenge/Standard.lean, which imports Mathlib only, repeats it word for word, so that the local monomialization of a real-analytic function (exists_proper_analytic_monomialization) can be stated there.

def IsMonomialAt (n : ℕ) {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (g : M → ℝ) (p : M) : Prop

A real function g on an n-dimensional manifold M is a monomial at p, up to a unit, if near p, in the coordinates y of the chart of M at p, g = u · y^α for an exponent vector α and a real-analytic function u that does not vanish at p.

Equations

• One or more equations did not get rendered due to their size.