Theorems · Definition · commutative algebra
MulSemiringAction.charpoly
{B : Type u_2} →
(G : Type u_3) → [inst : CommRing B] → [inst_1 : Group G] → [MulSemiringAction G B] → [Fintype G] → B → Polynomial BCharacteristic polynomial of a finite group action on a ring.
- Defined in
- Mathlib.RingTheory.Invariant.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Fintypestatement and proof · cited by 7,736
- Groupstatement and proof · cited by 6,238
- Polynomialstatement · cited by 5,681
- Finset.univproof · cited by 3,473
- Finset.prodproof · cited by 2,356
- Polynomial.Xproof · cited by 1,639
- Polynomial.Cproof · cited by 1,598
- MulSemiringActionstatement and proof · cited by 423
Cited by11
Results whose statement or proof uses this declaration.
- Algebra.IsInvariant.isIntegralproof · cited by 6
- Ideal.IsFractionRing.normalproof · cited by 3
- Algebra.IsInvariant.charpoly_mem_liftsstatement and proof · cited by 3
- MulSemiringAction.eval_charpolystatement · cited by 3
- MulSemiringAction.monic_charpolystatement · cited by 2
- MulSemiringAction.smul_charpolystatement · cited by 1
- MulSemiringAction.smul_coeff_charpolystatement and proof · cited by 1
- MulSemiringAction.splits_charpolystatement · cited by 1
- MulSemiringAction.charpoly_eqstatement · cited by 1
- MulSemiringAction.charpoly_eq_prod_smulstatement · cited by 1
- Ideal.Quotient.exists_algHom_fixedPoint_quotient_underproof · cited by 1