feat(RingTheory): generalize relNorm_eq_pow_of_isMaximal to separable fraction field extensions

[vaca22]

This PR relaxes the hypothesis of Ideal.relNorm_eq_pow_of_isMaximal and its supporting Ring.NormalClosure instances.
Originally the theorem required the fraction ring of base Dedekind domain R to be a perfect field. Now we only require the fraction field extension to be separable.
The perfect field condition excludes function fields with imperfect constant fields, which is an important case we want to support. The core mathematical insight is that the normal closure of a separable field extension stays separable, so we can construct the Galois structure without a perfect base.
This change is fully backwards compatible: any existing code relying on the old perfect field assumption still compiles, since perfect fields automatically give separable extensions. Only two files are modified: NormalClosure.lean and RelNorm.lean, with small diff and no extra imports.
AI disclosure: I used AI tools to assist with initial code drafting and full CI validation. All mathematical reasoning and proof logic I worked through independently, and I can explain every adjustment in review. My original PR text relied too heavily on AI output, I’ve fully rewritten this description manually.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 6c04ccae53

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ IntermediateField.normalClosure.isSeparable
+ IsGalois.normalClosure_of_isSeparable

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 6c04cca).

• +2 new declarations
• −0 removed declarations

+IntermediateField.normalClosure.isSeparable
+IsGalois.normalClosure_of_isSeparable

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 6c04ccae53
Reference commit 9b53612f8d

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[felixpernegger]

LLM-generated

[felixpernegger]

@vaca22 if you take a look at the AI guidelines, you shouldnt write PR descriptions entirely with AI. Maybe you can rewrite it with your own words?

[vaca22]

@vaca22 if you take a look at the AI guidelines, you shouldnt write PR descriptions entirely with AI. Maybe you can rewrite it with your own words?

Thanks a lot for pointing this out, I totally understand the guideline about avoiding fully AI-written PR descriptions.
All the math proofs and refactoring logic I re-derived and verified on my own, I just over-relied on AI to draft the full PR text initially.
I’ve rewritten the entire description with my own words now to fix this issue.

[xroblot]

Please fix the CI error (you probably just need to merge master)

[vaca22]

Fixed — merging master resolved the CI cache-verification error. All checks are green now, thanks!

[xroblot]

It is a nice generalization since IsSeparable is the right hypothesis here.

About the two new local instances: Normal K E is already an instance for a normal closure, but the fact that the normal closure of a separable extension is separable is missing. Thus you should add a new general instance:

instance [Algebra.IsSeparable F K] : IsGalois F (normalClosure F K L) where
    to_isSeparable := (your proof)
    to_normal := inferInstance

That way, IsGalois K E resolves directly (and you get Algebra.IsSeparable K E for free through the projection), so both local instances can go.

[vaca22]

It is a nice generalization since IsSeparable is the right hypothesis here.

About the two new local instances: Normal K E is already an instance for a normal closure, but the fact that the normal closure of a separable extension is separable is missing. Thus you should add a new general instance:

instance [Algebra.IsSeparable F K] : IsGalois F (normalClosure F K L) where
    to_isSeparable := (your proof)
    to_normal := inferInstance

That way, IsGalois K E resolves directly (and you get Algebra.IsSeparable K E for free through the projection), so both local instances can go.

Thanks, done. I split it into IntermediateField.normalClosure.isSeparable and IsGalois.normalClosure_of_isSeparable, and kept the existing IsGalois.normalClosure since [IsGalois k F] doesn't give Algebra.IsSeparable k K by instance search. Both local instances are gone.

[xroblot]

!radar

[leanprover-radar]

Benchmark results for 6c04cca against 9b53612 are in. No significant results found. @xroblot

• ✅ build//instructions: -288.1G (-0.20%)

Medium changes (1✅)

• 1 hidden

[xroblot]

Suggested change

	/-- Let $F / K / k$ be a tower of field extensions. If $K$ is separable over $k$,
	then the normal closure of $K$ over $k$ in $F$ is separable over $k$. -/
	instance IntermediateField.normalClosure.isSeparable [Algebra.IsSeparable k K] :
	Algebra.IsSeparable k (normalClosure k K F) := by
	rw [← le_separableClosure_iff]
	refine normalClosure_le_iff.mpr fun f ↦ ?_
	have : Algebra.IsSeparable k f.fieldRange :=
	AlgEquiv.Algebra.isSeparable (AlgEquiv.ofInjectiveField f)
	exact le_separableClosure k F f.fieldRange
	/-- Let `F / K / k` be a tower of field extensions. If `K` is separable over `k`,
	then the normal closure of `K/k` in `F` is separable over `k`. -/
	instance IntermediateField.normalClosure.isSeparable [Algebra.IsSeparable k K] :
	Algebra.IsSeparable k (normalClosure k K F) := by
	refine (le_separableClosure_iff _ _ _).mp <| normalClosure_le_iff.mpr fun f ↦ ?_
	have : Algebra.IsSeparable k f.fieldRange :=
	AlgEquiv.Algebra.isSeparable (AlgEquiv.ofInjectiveField f)
	exact le_separableClosure k F f.fieldRange

[xroblot]

Actually, it seems the $ notation is also used in this file so you can disregard the part about the docstring