Commit 2026-06-04 13:23 f98c28ed
View on Github →feat(RingTheory/Invariant/Basic): add isomorphism version of IsFractionRing.stabilizerHom (#40203)
This PR adds the isomorphism version of IsFractionRing.stabilizerHom (we already have the isomorphism version of Ideal.Quotient.stabilizerHom).
I had to switch from (inertia M P).subgroupOf (MulAction.stabilizer M P) to P.inertia (MulAction.stabilizer M P) since the latter is the simp normal form (and the linter was complaining).