Theorems · Theorem · group theory

CommGroup.forall_monoidHom_apply_eq_one_iff

∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G) (x : G),
  (∀ (φ : G →* Mˣ), (∀ y ∈ H, φ y = 1) → φ x = 1) ↔ x ∈ H

Defined in

Mathlib.GroupTheory.FiniteAbelian.Duality

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommGroupFiniteCommMonoidHasEnoughRootsOfUnity