Theorems · Theorem · group theory

Set.mulIndicator_sdiff

∀ {α : Type u_1} {G : Type u_6} [inst : Group G] {s t : Set α},
  s ⊆ t → ∀ (f : α → G), (t \ s).mulIndicator f = t.mulIndicator f * (s.mulIndicator f)⁻¹

Defined in

Mathlib.Algebra.Group.Indicator

Cited by

2 results in Mathlib

Foundations

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

Assumes

Group