LeanPool.OrderPQ.MulZMod #

source

def MulZMod (n : ℕ) :

Type

ZMod n viewed as a multiplicative group.

Equations

MulZMod n = Multiplicative (ZMod n)

Instances For

source

@[implicit_reducible]

instance instDecidableEqMulZMod {n : ℕ} :

DecidableEq (MulZMod n)

Equations

instDecidableEqMulZMod = instDecidableEqMultiplicative

source

@[implicit_reducible]

instance instFintypeMulZModOfNeZeroNat {n : ℕ} [NeZero n] :

Fintype (MulZMod n)

Equations

instFintypeMulZModOfNeZeroNat = Multiplicative.fintype

source

@[implicit_reducible]

instance instMulMulZMod {n : ℕ} :

Mul (MulZMod n)

Equations

instMulMulZMod = Multiplicative.mul

source

@[implicit_reducible]

instance instMulOneClassMulZMod {n : ℕ} :

MulOneClass (MulZMod n)

Equations

instMulOneClassMulZMod = Multiplicative.mulOneClass

source

@[implicit_reducible]

instance instGroupMulZMod {n : ℕ} :

Group (MulZMod n)

Equations

instGroupMulZMod = Multiplicative.group

source

instance instIsCyclicMulZMod {n : ℕ} :

IsCyclic (MulZMod n)

source

@[simp]

theorem card_mulZMod {n : ℕ} [NeZero n] :

Fintype.card (MulZMod n) = n

source

theorem nat_card_mulZMod {n : ℕ} [NeZero n] :

Nat.card (MulZMod n) = n

source

def unitOfNeZero {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ZMod p) (hx : x ≠ 0) :

(ZMod p)ˣ

A nonzero element of ZMod p (with p prime) viewed as a unit.

Equations

unitOfNeZero x hx = ZMod.unitOfCoprime x.val ⋯

Instances For

source

@[simp]

theorem val_unitOfNeZero {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ZMod p) (hx : x ≠ 0) :

↑(unitOfNeZero x hx) = x

source

@[simp]

theorem unitOfNeZero_val {p : ℕ} [hp : Fact (Nat.Prime p)] (x : (ZMod p)ˣ) :

unitOfNeZero ↑x ⋯ = x

source

def addAutOfUnit {p : ℕ} [hp : Fact (Nat.Prime p)] (x : (ZMod p)ˣ) :

AddAut (ZMod p)

Multiplication by a unit in ZMod p as an additive automorphism.

Equations

addAutOfUnit x = { toFun := fun (a : ZMod p) => ↑x * a, invFun := fun (a : ZMod p) => x.inv * a, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source

theorem addAutOfUnit_symm_apply {p : ℕ} [hp : Fact (Nat.Prime p)] (x : (ZMod p)ˣ) (a : ZMod p) :

(AddEquiv.symm (addAutOfUnit x)) a = x.inv * a

source

theorem addAutOfUnit_apply {p : ℕ} [hp : Fact (Nat.Prime p)] (x : (ZMod p)ˣ) (a : ZMod p) :

(addAutOfUnit x) a = ↑x * a

source

def mulEquivAddAutZMod (p : ℕ) [hp : Fact (Nat.Prime p)] :

AddAut (ZMod p) ≃+ Additive (ZMod p)ˣ

The group of additive automorphisms of ZMod p (with p prime) is isomorphic to the group of units of ZMod p.

Equations

mulEquivAddAutZMod p = ZMod.AddAutEquivUnits p

Instances For

source

def mulEquivMulAutMulZMod (p : ℕ) [hp : Fact (Nat.Prime p)] :

MulAut (MulZMod p) ≃* (ZMod p)ˣ

The group of multiplicative automorphisms of MulZMod p (with p prime) is isomorphic to the group of units of ZMod p.

Equations

mulEquivMulAutMulZMod p = (MulAutMultiplicative (ZMod p)).trans (AddEquiv.toMultiplicativeLeft (mulEquivAddAutZMod p))

Instances For

source

@[implicit_reducible]

noncomputable instance instFintypeMulAutMulZMod (p : ℕ) [hp : Fact (Nat.Prime p)] :

Fintype (MulAut (MulZMod p))

Equations

instFintypeMulAutMulZMod p = Fintype.ofEquiv (ZMod p)ˣ (mulEquivMulAutMulZMod p).symm.toEquiv

source

theorem mulAut_MulZMod_isCyclic (p : ℕ) [hp : Fact (Nat.Prime p)] :

IsCyclic (MulAut (MulZMod p))

source

theorem addAut_ZMod_isCyclic (p : ℕ) [hp : Fact (Nat.Prime p)] :

IsCyclic (Multiplicative (AddAut (ZMod p)))

source

@[simp]

theorem card_mulAut_mulZMod (p : ℕ) [hp : Fact (Nat.Prime p)] :

Fintype.card (MulAut (MulZMod p)) = p - 1

source

theorem nat_card_mulAut_mulZMod (p : ℕ) [hp : Fact (Nat.Prime p)] :

Nat.card (MulAut (MulZMod p)) = p - 1