SchemeTheory.stabilizerLocalization_inertia_card
The actual local inertia used by the ring character has the original ideal-inertia order. The comparison introduces no residue-field structure.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace SchemeTheory
universe u vLean source · statement
theorem stabilizerLocalization_inertia_card
(B : Type u) [CommRing B] (G : Type v) [Group G] [MulSemiringAction G B]
(Q : Ideal B) [Q.IsPrime] :
Nat.card ((IsLocalRing.maximalIdeal (Localization.AtPrime Q)).inertia
(MulAction.stabilizer G Q)) = Nat.card (Q.inertia G)