mathlib3 documentation

data.zmod.defs

Definition of `zmod n` + basic results. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides the basic details of zmod n, including its commutative ring structure.

Implementation details #

This used to be inlined into data/zmod/basic.lean. This file imports char_p/basic, which is an issue; all char_p instances create an algebra (zmod p) R instance; however, this instance may not be definitionally equal to other algebra instances (for example, galois_field also has an algebra instance as it is defined as a splitting_field). The way to fix this is to use the forgetful inheritance pattern, and make char_p carry the data of what the smul should be (so for example, the smul on the galois_field char_p instance should be equal to the smul from its splitting_field structure); there is only one possible zmod p algebra for any p, so this is not an issue mathematically. For this to be possible, however, we need char_p/basic to be able to import some part of zmod.

Ring structure on `fin n` #

We define a commutative ring structure on fin n, but we do not register it as instance. Afterwords, when we define zmod n in terms of fin n, we use these definitions to register the ring structure on zmod n as type class instance.

@[protected, instance]

def fin.comm_semigroup (n : ℕ) :

comm_semigroup (fin n)

Multiplicative commutative semigroup structure on fin n.

Equations

fin.comm_semigroup n = {mul := has_mul.mul fin.has_mul, mul_assoc := _, mul_comm := _}

@[protected, instance]

def fin.distrib (n : ℕ) :

distrib (fin n)

Equations

fin.distrib n = {mul := comm_semigroup.mul (fin.comm_semigroup n), add := add_comm_semigroup.add (fin.add_comm_semigroup n), left_distrib := _, right_distrib := _}

@[protected, instance]

def fin.comm_ring (n : ℕ) [ne_zero n] :

comm_ring (fin n)

Commutative ring structure on fin n.

Equations

fin.comm_ring n = {add := add_monoid_with_one.add fin.add_monoid_with_one, add_assoc := _, zero := add_monoid_with_one.zero fin.add_monoid_with_one, zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul fin.add_monoid_with_one, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (fin.add_comm_group n), sub := add_comm_group.sub (fin.add_comm_group n), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (fin.add_comm_group n), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast._default add_monoid_with_one.nat_cast add_monoid_with_one.add _ add_monoid_with_one.zero _ _ add_monoid_with_one.nsmul _ _ add_monoid_with_one.one _ _ add_comm_group.neg add_comm_group.sub _ add_comm_group.zsmul _ _ _ _, nat_cast := add_monoid_with_one.nat_cast fin.add_monoid_with_one, one := add_monoid_with_one.one fin.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_semigroup.mul (fin.comm_semigroup n), mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow._default add_monoid_with_one.one comm_semigroup.mul fin.one_mul fin.mul_one, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

@[protected, instance]

def fin.has_distrib_neg (n : ℕ) :

has_distrib_neg (fin n)

Note this is more general than fin.comm_ring as it applies (vacuously) to fin 0 too.

Equations

fin.has_distrib_neg n = {neg := has_neg.neg (fin.has_neg n), neg_neg := _, neg_mul := _, mul_neg := _}

def zmod :

The integers modulo n : ℕ.

Equations

zmod (n + 1) = fin (n + 1)
zmod 0 = ℤ

Instances for zmod

@[protected, instance]

def zmod.decidable_eq (n : ℕ) :

decidable_eq (zmod n)

Equations

zmod.decidable_eq (n + 1) = fin.decidable_eq (n.add 0 + 1)
zmod.decidable_eq 0 = int.decidable_eq

@[protected, instance]

def zmod.has_repr (n : ℕ) :

has_repr (zmod n)

Equations

zmod.has_repr (n + 1) = fin.has_repr (n.add 0 + 1)
zmod.has_repr 0 = int.has_repr

@[protected, instance]

def zmod.fintype (n : ℕ) [ne_zero n] :

fintype (zmod n)

Equations

zmod.fintype (n + 1) = fin.fintype (n + 1)
zmod.fintype 0 = _.elim

@[protected, instance]

def zmod.infinite :

infinite (zmod 0)

@[simp]

theorem zmod.card (n : ℕ) [fintype (zmod n)] :

fintype.card (zmod n) = n

@[protected, instance]

def zmod.comm_ring (n : ℕ) :

comm_ring (zmod n)

Equations

zmod.comm_ring n = {add := n.cases_on has_add.add (λ (n : ℕ), has_add.add), add_assoc := _, zero := n.cases_on 0 (λ (n : ℕ), 0), zero_add := _, add_zero := _, nsmul := n.cases_on comm_ring.nsmul (λ (n : ℕ), comm_ring.nsmul), nsmul_zero' := _, nsmul_succ' := _, neg := n.cases_on has_neg.neg (λ (n : ℕ), has_neg.neg), sub := n.cases_on has_sub.sub (λ (n : ℕ), has_sub.sub), sub_eq_add_neg := _, zsmul := n.cases_on comm_ring.zsmul (λ (n : ℕ), comm_ring.zsmul), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := n.cases_on coe (λ (n : ℕ), coe), nat_cast := n.cases_on coe (λ (n : ℕ), coe), one := n.cases_on 1 (λ (n : ℕ), 1), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := n.cases_on has_mul.mul (λ (n : ℕ), has_mul.mul), mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow._default (n.cases_on 1 (λ (n : ℕ), 1)) (n.cases_on has_mul.mul (λ (n : ℕ), has_mul.mul)) _ _, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

@[protected, instance]

def zmod.inhabited (n : ℕ) :

inhabited (zmod n)

Equations

zmod.inhabited n = {default := 0}