Theorems · Theorem · ring theory

Set.zero_mem_smul_iff

∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : AddCommMonoid β] [inst_2 : Module α β] [IsDomain α]
  [Module.IsTorsionFree α β] {s : Set α} {t : Set β}, 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Defined in

Mathlib.Algebra.Ring.Action.Pointwise.Set

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleIsDomainModule.IsTorsionFree