Commit 2025-09-27 10:51 528d3ce5

View on Github →

feat(RingTheory/Invariant): residue field extension is finite (#25616)

Estimated changes

Modified Mathlib/FieldTheory/Galois/Basic.lean

added theorem IsGalois.finiteDimensional_of_finite

Modified Mathlib/RingTheory/Invariant/Basic.lean

added theorem Ideal.Quotient.finite_of_isInvariant

added theorem Ideal.Quotient.normal