Theorems · Theorem · ring theory

SkewMonoidAlgebra.support_single_mul_eq_image

∀ {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 : DecidableEq G] {r : k} {x : G},
  IsLeftRegular x →
    (∀ (y : k), r * x • y = 0 ↔ y = 0) →
      (SkewMonoidAlgebra.single x r * f).support = Finset.image (fun x_1 => x * x_1) f.support

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Support

Cited by

1 results in Mathlib

Foundations

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

Assumes

MonoidSemiringMulSemiringActionDecidableEq