Commit 2026-03-10 12:49 b4e4e502

chore: remove unnecessary private and backward.privateInPublic (#36430) This PR removes private modifiers and corresponding set_option backward.privateInPublic from definitions in three files where they are not really sensible. These private definitions were being exposed to public proofs via backward.privateInPublic, which means the private names (with _private. mangling) appear in downstream goal states. When the tactic analysis regression linter tries to re-run replacement tactics on those goals, it encounters "Unknown constant" errors because the private constants aren't accessible from other modules. Files changed:

• Mathlib.RingTheory.OreLocalization.Basic: remove private from add'', add''_char, add', add, nsmul
• Mathlib.Analysis.Complex.Norm: change private to protected for norm_nonneg, norm_add_le', norm_eq_zero_iff, norm_map_zero', norm_neg' (these names clash with global names from NormedAddCommGroup)
• Mathlib.Analysis.Normed.Module.Multilinear.Basic: remove private from uniformity_eq_seminorm Verified locally: all three files and their downstream dependencies build successfully. 🤖 Prepared with Claude Code