Theorems · Definition · number theory

MulChar.subgroupOrderIsoSubgroupMulChar

(M : Type u_1) →
  (R : Type u_2) →
    [inst : CommMonoid M] →
      [inst_1 : CommRing R] →
        [Finite M] → [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] → Subgroup Mˣ ≃o (Subgroup (MulChar M R))ᵒᵈ

The order reversing bijection that sends a subgroup of Mˣ to its dual subgroup in MulChar M R where M is a finite commutative monoid and R is a ring with enough roots of unity.

Defined in

Mathlib.NumberTheory.MulChar.Duality

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommMonoidCommRingFiniteHasEnoughRootsOfUnity