Commit 2026-08-18 10:50 ca3a90d0

View on Github →

chore(FieldTheory/Galois/IsGaloisGroup): remove FaithfulSMul assumptions (#41208) A few results in IsGaloisGroup.lean are proved by passing to fraction fields which requires assuming FaithfulSMul. This PR removes the FaithfulSMul assumption by first passing to the image subring.

Estimated changes

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

modified theorem IsGaloisGroup.card_eq_finrank'

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

Modified Mathlib/RingTheory/IsGaloisGroup/Basic.lean