Theorems · Theorem · group theory

Set.apply_mulIndicator_symmDiff

∀ {α : Type u_1} {β : Type u_2} {G : Type u_6} [inst : Group G] {g : G → β},
  (∀ (x : G), g x⁻¹ = g x) →
    ∀ (s t : Set α) (f : α → G) (x : α),
      g ((symmDiff s t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Defined in

Mathlib.Algebra.Group.Indicator

Cited by

2 results in Mathlib

Foundations

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

Assumes

Group