The strict transform is generated by the strict transforms of the elements

[BM97, Proposition 3.13]: the stalk of the strict transform X' at a' is generated by the strict transforms y^{-d}(f ∘ π) of the elements f ∈ I_{π(a')} (strictTransform_eq_span_strictTransformElems). The stalk of X' is, by the finite type of the saturation (saturation_hasLocalGenerators, Hironaka/AnalyticSpace/Noether/Saturation.lean), the saturation ⋃_k (π⁻¹(I)_{a'} : I_{F,a'}^k) of the total transform with respect to the exceptional divisor (stalkIdeal_strictTransformSubspace_of_hasLocalGenerators); that the saturation is generated by the strict transforms of the elements is saturationStalk_eq_span_strictTransformElems of Hironaka/Manifold/BlowUp/Transform/StrictSubspaceCompletion.lean. Nothing but the root aggregator imports this module.

The argument differs from Bierstone and Milman's. In the printed proof of Proposition 3.13 the vertices of the diagram of initial exponents are represented by F_i := ∑_j P_{ij} (H_j ∘ σ) with polynomial coefficients P_{ij} ∈ k[Y], and the only division is by the power Y_1^{q_i}; the library does not follow that argument (it could not verify the existence of polynomial coefficients for the order of [BM97, Lemma 3.22]; Hironaka/Manifold/BlowUp/Transform/StrictSubspaceProp313.lean) and argues by flatness instead. Off the centre both sides are π⁻¹(I)_{a'}; over the centre, in a blow-up chart of index i with the coordinates shifted at a', the chart ring R' = R[x_j/x_r] (chartRingOf, Hironaka/Algebra/Local/ChartRing.lean) maps to 𝒪_{M',a'} by a homomorphism χ (Hironaka/Algebra/Local/ChartHom.lean), the saturation is ⋃_k (χ(I R') : χ(x_r)^k), and this is χ(⋃_k (I R' : x_r^k)) because the saturation of R' descends from the completion 𝒪̂_{M',a'}, which is flat over R' — R'_{𝔪'} → 𝒪_{M',a'} induces an isomorphism of completions, both 𝕜⟦X⟧ by Cohen's structure theorem (Hironaka/Algebra/Local/ChartCompletionHom.lean, Hironaka/Algebra/SaturationDescent.lean) — and ⋃_k (I R' : x_r^k) is the ideal of the transforms x_r^{-M} φ(f) (Hironaka/Algebra/Local/ChartSaturation.lean), whose images χ(g) satisfy u_{σ i}^M χ(g) = f ∘ π: strict transforms of elements.

theorem AnalyticSpace.strictTransform_eq_span_strictTransformElems {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (a' : M') : (Manifold.strictTransformSubspace hY h I).stalkIdeal a' = Ideal.span (Manifold.strictTransformElems hY h I a')

The strict transform is generated by the strict transforms of the elements [BM97, Proposition 3.13]: the stalk of X' at a' is spanned by the y^{-d}(f ∘ π), f ∈ I_{π(a')}.