Theorems · Theorem · group theory

Set.mulIndicator_div

∀ {α : Type u_1} {G : Type u_6} [inst : Group G] (s : Set α) (f g : α → G),
  (s.mulIndicator fun a => f a / g a) = fun a => s.mulIndicator f a / s.mulIndicator g a

Defined in

Mathlib.Algebra.Group.Indicator

Cited by

1 results in Mathlib

Foundations

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

Assumes

Group