Theorems · Theorem · ring theory

SkewMonoidAlgebra.support_single_mul

∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Semiring k] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) [inst_3 : IsLeftCancelMul G] (r : k) (x : G),
  (∀ (y : k), r * x • y = 0 ↔ y = 0) →
    (SkewMonoidAlgebra.single x r * f).support = Finset.map (mulLeftEmbedding x) f.support

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Support

Cited by

0 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidSemiringMulSemiringActionIsLeftCancelMul