Theorems · Definition · commutative algebra
prodXSubSMul
(G : Type u_2) → [inst : Group G] → [Fintype G] → (R : Type u_3) → [inst_2 : CommRing R] → [MulSemiringAction G R] → R → Polynomial R
the product of (X - g • x) over distinct g • x.
- Cited by
- 7 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.
Cites13
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
- HasQuotient.Quotientproof · cited by 2,301
- Polynomial.Xproof · cited by 1,639
- Polynomial.Cproof · cited by 1,598
- MulSemiringActionstatement and proof · cited by 423
- MulAction.stabilizerproof · cited by 254
Cited by8
Results whose statement or proof uses this declaration.
- FixedPoints.minpolyproof · cited by 9
- FixedPoints.minpoly.eval₂proof · cited by 5
- FixedPoints.minpoly.monicproof · cited by 4
- prodXSubSMul.evalstatement · cited by 1
- prodXSubSMul.monicstatement · cited by 1
- prodXSubSMul.smulstatement · cited by 1
- FixedPoints.minpoly.of_eval₂proof · cited by 1
- prodXSubSMul.coeffstatement and proof · cited by 0