Theorems · Theorem · group theory

Set.mem_invOf_smul_set

∀ {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : MulAction α β] {s : Set β} {a : α} {b : β}
  [inst_2 : Invertible a], b ∈ ⅟a • s ↔ a • b ∈ s

Defined in

Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Cited by

0 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

MonoidMulActionInvertible