Documentation

HironakaExamples.Balanced.PowerSeriesTwoVariables

D-balance and MC-invariance of ⟨x₀^m⟩ and ⟨x₀ x₁⟩ in ℚ⟦x₀, x₁⟧ #

The two examples of Hironaka/Algebra/Local/Balanced.lean and MaximalContact.lean on the coordinate structure RegularCoords.mvPowerSeries of ℚ⟦x₀, x₁⟧, whose regularity and dimension inputs are Hironaka/Algebra/Local/PowerSeriesRegular.lean: ⟨x₀^m⟩ is D-balanced with respect to m and MC-invariant with respect to m ≥ 1, and ⟨x₀ x₁⟩ is neither with respect to 2.