Theorem MulSemiringAction.splits_charpoly

Modification history

2026-06-15 13:16

Mathlib/RingTheory/Invariant/Basic.lean

feat(RingTheory/Invariant/Basic): generalize `Ideal.Quotient.normal` to `IsFractionRing` (#40247) …

Added MulSemiringAction.splits_charpoly View on Github →