Theorems · Theorem · ring theory
MonoidAlgebra.support_single_mul
Deprecated since 2026-06-18Use MonoidAlgebra.support_coeff_single_mul instead.
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : IsLeftCancelMul G] (f : MonoidAlgebra k G)
(r : k),
(∀ (y : k), r * y = 0 ↔ y = 0) →
∀ (x : G), (MonoidAlgebra.single x r * f).coeff.support = Finset.map (mulLeftEmbedding x) f.coeff.supportAlias of MonoidAlgebra.support_coeff_single_mul.
- Defined in
- Mathlib.Algebra.MonoidAlgebra.Support
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringMulIsLeftCancelMul
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.
- Semiringstatement · cited by 13,802
- Finsetstatement · cited by 13,712
- Finsupp.supportstatement · cited by 828
- Finset.mapstatement · cited by 747
- MonoidAlgebrastatement · cited by 590
- MonoidAlgebra.singlestatement · cited by 253
- MonoidAlgebra.coeffstatement · cited by 224
- IsLeftCancelMulstatement · cited by 51
- mulLeftEmbeddingstatement · cited by 8
- MonoidAlgebra.support_coeff_single_mulproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.