HexGFqMathlib.Embeddings.S0

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_2 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 2 Hex.Conway.supportedEntry_2_2

The canonical embedding of GF(2^1) into GF(2^2).

Equations

HexGFqMathlib.Conway.embed_2_1_2 = HexGFqMathlib.conwayEmbed 2 1 2 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_2 Hex.Conway.compat_2_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_3 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 3 Hex.Conway.supportedEntry_2_3

The canonical embedding of GF(2^1) into GF(2^3).

Equations

HexGFqMathlib.Conway.embed_2_1_3 = HexGFqMathlib.conwayEmbed 2 1 3 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_3 Hex.Conway.compat_2_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_4 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 4 Hex.Conway.supportedEntry_2_4

The canonical embedding of GF(2^1) into GF(2^4).

Equations

HexGFqMathlib.Conway.embed_2_1_4 = HexGFqMathlib.conwayEmbed 2 1 4 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_4 Hex.Conway.compat_2_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_2_4 :

Hex.GFq 2 2 Hex.Conway.supportedEntry_2_2 →+* Hex.GFq 2 4 Hex.Conway.supportedEntry_2_4

The canonical embedding of GF(2^2) into GF(2^4).

Equations

HexGFqMathlib.Conway.embed_2_2_4 = HexGFqMathlib.conwayEmbed 2 2 4 Hex.Conway.supportedEntry_2_2 Hex.Conway.supportedEntry_2_4 Hex.Conway.compat_2_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_5 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 5 Hex.Conway.supportedEntry_2_5

The canonical embedding of GF(2^1) into GF(2^5).

Equations

HexGFqMathlib.Conway.embed_2_1_5 = HexGFqMathlib.conwayEmbed 2 1 5 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_5 Hex.Conway.compat_2_1_5

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_6 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 6 Hex.Conway.supportedEntry_2_6

The canonical embedding of GF(2^1) into GF(2^6).

Equations

HexGFqMathlib.Conway.embed_2_1_6 = HexGFqMathlib.conwayEmbed 2 1 6 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_6 Hex.Conway.compat_2_1_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_2_6 :

Hex.GFq 2 2 Hex.Conway.supportedEntry_2_2 →+* Hex.GFq 2 6 Hex.Conway.supportedEntry_2_6

The canonical embedding of GF(2^2) into GF(2^6).

Equations

HexGFqMathlib.Conway.embed_2_2_6 = HexGFqMathlib.conwayEmbed 2 2 6 Hex.Conway.supportedEntry_2_2 Hex.Conway.supportedEntry_2_6 Hex.Conway.compat_2_2_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_3_6 :

Hex.GFq 2 3 Hex.Conway.supportedEntry_2_3 →+* Hex.GFq 2 6 Hex.Conway.supportedEntry_2_6

The canonical embedding of GF(2^3) into GF(2^6).

Equations

HexGFqMathlib.Conway.embed_2_3_6 = HexGFqMathlib.conwayEmbed 2 3 6 Hex.Conway.supportedEntry_2_3 Hex.Conway.supportedEntry_2_6 Hex.Conway.compat_2_3_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_7 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 7 Hex.Conway.supportedEntry_2_7

The canonical embedding of GF(2^1) into GF(2^7).

Equations

HexGFqMathlib.Conway.embed_2_1_7 = HexGFqMathlib.conwayEmbed 2 1 7 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_7 Hex.Conway.compat_2_1_7

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_8 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 8 Hex.Conway.supportedEntry_2_8

The canonical embedding of GF(2^1) into GF(2^8).

Equations

HexGFqMathlib.Conway.embed_2_1_8 = HexGFqMathlib.conwayEmbed 2 1 8 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_8 Hex.Conway.compat_2_1_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_2_8 :

Hex.GFq 2 2 Hex.Conway.supportedEntry_2_2 →+* Hex.GFq 2 8 Hex.Conway.supportedEntry_2_8

The canonical embedding of GF(2^2) into GF(2^8).

Equations

HexGFqMathlib.Conway.embed_2_2_8 = HexGFqMathlib.conwayEmbed 2 2 8 Hex.Conway.supportedEntry_2_2 Hex.Conway.supportedEntry_2_8 Hex.Conway.compat_2_2_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_4_8 :

Hex.GFq 2 4 Hex.Conway.supportedEntry_2_4 →+* Hex.GFq 2 8 Hex.Conway.supportedEntry_2_8

The canonical embedding of GF(2^4) into GF(2^8).

Equations

HexGFqMathlib.Conway.embed_2_4_8 = HexGFqMathlib.conwayEmbed 2 4 8 Hex.Conway.supportedEntry_2_4 Hex.Conway.supportedEntry_2_8 Hex.Conway.compat_2_4_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_9 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 9 Hex.Conway.supportedEntry_2_9

The canonical embedding of GF(2^1) into GF(2^9).

Equations

HexGFqMathlib.Conway.embed_2_1_9 = HexGFqMathlib.conwayEmbed 2 1 9 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_9 Hex.Conway.compat_2_1_9

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_3_9 :

Hex.GFq 2 3 Hex.Conway.supportedEntry_2_3 →+* Hex.GFq 2 9 Hex.Conway.supportedEntry_2_9

The canonical embedding of GF(2^3) into GF(2^9).

Equations

HexGFqMathlib.Conway.embed_2_3_9 = HexGFqMathlib.conwayEmbed 2 3 9 Hex.Conway.supportedEntry_2_3 Hex.Conway.supportedEntry_2_9 Hex.Conway.compat_2_3_9

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_10 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 10 Hex.Conway.supportedEntry_2_10

The canonical embedding of GF(2^1) into GF(2^10).

Equations

HexGFqMathlib.Conway.embed_2_1_10 = HexGFqMathlib.conwayEmbed 2 1 10 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_10 Hex.Conway.compat_2_1_10

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_2_10 :

Hex.GFq 2 2 Hex.Conway.supportedEntry_2_2 →+* Hex.GFq 2 10 Hex.Conway.supportedEntry_2_10

The canonical embedding of GF(2^2) into GF(2^10).

Equations

HexGFqMathlib.Conway.embed_2_2_10 = HexGFqMathlib.conwayEmbed 2 2 10 Hex.Conway.supportedEntry_2_2 Hex.Conway.supportedEntry_2_10 Hex.Conway.compat_2_2_10

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_5_10 :

Hex.GFq 2 5 Hex.Conway.supportedEntry_2_5 →+* Hex.GFq 2 10 Hex.Conway.supportedEntry_2_10

The canonical embedding of GF(2^5) into GF(2^10).

Equations

HexGFqMathlib.Conway.embed_2_5_10 = HexGFqMathlib.conwayEmbed 2 5 10 Hex.Conway.supportedEntry_2_5 Hex.Conway.supportedEntry_2_10 Hex.Conway.compat_2_5_10

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_11 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 11 Hex.Conway.supportedEntry_2_11

The canonical embedding of GF(2^1) into GF(2^11).

Equations

HexGFqMathlib.Conway.embed_2_1_11 = HexGFqMathlib.conwayEmbed 2 1 11 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_11 Hex.Conway.compat_2_1_11

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_12 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 12 Hex.Conway.supportedEntry_2_12

The canonical embedding of GF(2^1) into GF(2^12).

Equations

HexGFqMathlib.Conway.embed_2_1_12 = HexGFqMathlib.conwayEmbed 2 1 12 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_12 Hex.Conway.compat_2_1_12

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_2_12 :

Hex.GFq 2 2 Hex.Conway.supportedEntry_2_2 →+* Hex.GFq 2 12 Hex.Conway.supportedEntry_2_12

The canonical embedding of GF(2^2) into GF(2^12).

Equations

HexGFqMathlib.Conway.embed_2_2_12 = HexGFqMathlib.conwayEmbed 2 2 12 Hex.Conway.supportedEntry_2_2 Hex.Conway.supportedEntry_2_12 Hex.Conway.compat_2_2_12

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_3_12 :

Hex.GFq 2 3 Hex.Conway.supportedEntry_2_3 →+* Hex.GFq 2 12 Hex.Conway.supportedEntry_2_12

The canonical embedding of GF(2^3) into GF(2^12).

Equations

HexGFqMathlib.Conway.embed_2_3_12 = HexGFqMathlib.conwayEmbed 2 3 12 Hex.Conway.supportedEntry_2_3 Hex.Conway.supportedEntry_2_12 Hex.Conway.compat_2_3_12

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_4_12 :

Hex.GFq 2 4 Hex.Conway.supportedEntry_2_4 →+* Hex.GFq 2 12 Hex.Conway.supportedEntry_2_12

The canonical embedding of GF(2^4) into GF(2^12).

Equations

HexGFqMathlib.Conway.embed_2_4_12 = HexGFqMathlib.conwayEmbed 2 4 12 Hex.Conway.supportedEntry_2_4 Hex.Conway.supportedEntry_2_12 Hex.Conway.compat_2_4_12

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_6_12 :

Hex.GFq 2 6 Hex.Conway.supportedEntry_2_6 →+* Hex.GFq 2 12 Hex.Conway.supportedEntry_2_12

The canonical embedding of GF(2^6) into GF(2^12).

Equations

HexGFqMathlib.Conway.embed_2_6_12 = HexGFqMathlib.conwayEmbed 2 6 12 Hex.Conway.supportedEntry_2_6 Hex.Conway.supportedEntry_2_12 Hex.Conway.compat_2_6_12

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_13 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 13 Hex.Conway.supportedEntry_2_13

The canonical embedding of GF(2^1) into GF(2^13).

Equations

HexGFqMathlib.Conway.embed_2_1_13 = HexGFqMathlib.conwayEmbed 2 1 13 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_13 Hex.Conway.compat_2_1_13

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_14 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 14 Hex.Conway.supportedEntry_2_14

The canonical embedding of GF(2^1) into GF(2^14).

Equations

HexGFqMathlib.Conway.embed_2_1_14 = HexGFqMathlib.conwayEmbed 2 1 14 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_14 Hex.Conway.compat_2_1_14

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_2_14 :

Hex.GFq 2 2 Hex.Conway.supportedEntry_2_2 →+* Hex.GFq 2 14 Hex.Conway.supportedEntry_2_14

The canonical embedding of GF(2^2) into GF(2^14).

Equations

HexGFqMathlib.Conway.embed_2_2_14 = HexGFqMathlib.conwayEmbed 2 2 14 Hex.Conway.supportedEntry_2_2 Hex.Conway.supportedEntry_2_14 Hex.Conway.compat_2_2_14

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_7_14 :

Hex.GFq 2 7 Hex.Conway.supportedEntry_2_7 →+* Hex.GFq 2 14 Hex.Conway.supportedEntry_2_14

The canonical embedding of GF(2^7) into GF(2^14).

Equations

HexGFqMathlib.Conway.embed_2_7_14 = HexGFqMathlib.conwayEmbed 2 7 14 Hex.Conway.supportedEntry_2_7 Hex.Conway.supportedEntry_2_14 Hex.Conway.compat_2_7_14

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_15 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 15 Hex.Conway.supportedEntry_2_15

The canonical embedding of GF(2^1) into GF(2^15).

Equations

HexGFqMathlib.Conway.embed_2_1_15 = HexGFqMathlib.conwayEmbed 2 1 15 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_15 Hex.Conway.compat_2_1_15

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_3_15 :

Hex.GFq 2 3 Hex.Conway.supportedEntry_2_3 →+* Hex.GFq 2 15 Hex.Conway.supportedEntry_2_15

The canonical embedding of GF(2^3) into GF(2^15).

Equations

HexGFqMathlib.Conway.embed_2_3_15 = HexGFqMathlib.conwayEmbed 2 3 15 Hex.Conway.supportedEntry_2_3 Hex.Conway.supportedEntry_2_15 Hex.Conway.compat_2_3_15

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_5_15 :

Hex.GFq 2 5 Hex.Conway.supportedEntry_2_5 →+* Hex.GFq 2 15 Hex.Conway.supportedEntry_2_15

The canonical embedding of GF(2^5) into GF(2^15).

Equations

HexGFqMathlib.Conway.embed_2_5_15 = HexGFqMathlib.conwayEmbed 2 5 15 Hex.Conway.supportedEntry_2_5 Hex.Conway.supportedEntry_2_15 Hex.Conway.compat_2_5_15

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_1_16 :

Hex.GFq 2 1 Hex.Conway.supportedEntry_2_1 →+* Hex.GFq 2 16 Hex.Conway.supportedEntry_2_16

The canonical embedding of GF(2^1) into GF(2^16).

Equations

HexGFqMathlib.Conway.embed_2_1_16 = HexGFqMathlib.conwayEmbed 2 1 16 Hex.Conway.supportedEntry_2_1 Hex.Conway.supportedEntry_2_16 Hex.Conway.compat_2_1_16

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_2_16 :

Hex.GFq 2 2 Hex.Conway.supportedEntry_2_2 →+* Hex.GFq 2 16 Hex.Conway.supportedEntry_2_16

The canonical embedding of GF(2^2) into GF(2^16).

Equations

HexGFqMathlib.Conway.embed_2_2_16 = HexGFqMathlib.conwayEmbed 2 2 16 Hex.Conway.supportedEntry_2_2 Hex.Conway.supportedEntry_2_16 Hex.Conway.compat_2_2_16

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_4_16 :

Hex.GFq 2 4 Hex.Conway.supportedEntry_2_4 →+* Hex.GFq 2 16 Hex.Conway.supportedEntry_2_16

The canonical embedding of GF(2^4) into GF(2^16).

Equations

HexGFqMathlib.Conway.embed_2_4_16 = HexGFqMathlib.conwayEmbed 2 4 16 Hex.Conway.supportedEntry_2_4 Hex.Conway.supportedEntry_2_16 Hex.Conway.compat_2_4_16

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_2_8_16 :

Hex.GFq 2 8 Hex.Conway.supportedEntry_2_8 →+* Hex.GFq 2 16 Hex.Conway.supportedEntry_2_16

The canonical embedding of GF(2^8) into GF(2^16).

Equations

HexGFqMathlib.Conway.embed_2_8_16 = HexGFqMathlib.conwayEmbed 2 8 16 Hex.Conway.supportedEntry_2_8 Hex.Conway.supportedEntry_2_16 Hex.Conway.compat_2_8_16

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_1_2 :

Hex.GFq 3 1 Hex.Conway.supportedEntry_3_1 →+* Hex.GFq 3 2 Hex.Conway.supportedEntry_3_2

The canonical embedding of GF(3^1) into GF(3^2).

Equations

HexGFqMathlib.Conway.embed_3_1_2 = HexGFqMathlib.conwayEmbed 3 1 2 Hex.Conway.supportedEntry_3_1 Hex.Conway.supportedEntry_3_2 Hex.Conway.compat_3_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_1_3 :

Hex.GFq 3 1 Hex.Conway.supportedEntry_3_1 →+* Hex.GFq 3 3 Hex.Conway.supportedEntry_3_3

The canonical embedding of GF(3^1) into GF(3^3).

Equations

HexGFqMathlib.Conway.embed_3_1_3 = HexGFqMathlib.conwayEmbed 3 1 3 Hex.Conway.supportedEntry_3_1 Hex.Conway.supportedEntry_3_3 Hex.Conway.compat_3_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_1_4 :

Hex.GFq 3 1 Hex.Conway.supportedEntry_3_1 →+* Hex.GFq 3 4 Hex.Conway.supportedEntry_3_4

The canonical embedding of GF(3^1) into GF(3^4).

Equations

HexGFqMathlib.Conway.embed_3_1_4 = HexGFqMathlib.conwayEmbed 3 1 4 Hex.Conway.supportedEntry_3_1 Hex.Conway.supportedEntry_3_4 Hex.Conway.compat_3_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_2_4 :

Hex.GFq 3 2 Hex.Conway.supportedEntry_3_2 →+* Hex.GFq 3 4 Hex.Conway.supportedEntry_3_4

The canonical embedding of GF(3^2) into GF(3^4).

Equations

HexGFqMathlib.Conway.embed_3_2_4 = HexGFqMathlib.conwayEmbed 3 2 4 Hex.Conway.supportedEntry_3_2 Hex.Conway.supportedEntry_3_4 Hex.Conway.compat_3_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_1_5 :

Hex.GFq 3 1 Hex.Conway.supportedEntry_3_1 →+* Hex.GFq 3 5 Hex.Conway.supportedEntry_3_5

The canonical embedding of GF(3^1) into GF(3^5).

Equations

HexGFqMathlib.Conway.embed_3_1_5 = HexGFqMathlib.conwayEmbed 3 1 5 Hex.Conway.supportedEntry_3_1 Hex.Conway.supportedEntry_3_5 Hex.Conway.compat_3_1_5

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_1_6 :

Hex.GFq 3 1 Hex.Conway.supportedEntry_3_1 →+* Hex.GFq 3 6 Hex.Conway.supportedEntry_3_6

The canonical embedding of GF(3^1) into GF(3^6).

Equations

HexGFqMathlib.Conway.embed_3_1_6 = HexGFqMathlib.conwayEmbed 3 1 6 Hex.Conway.supportedEntry_3_1 Hex.Conway.supportedEntry_3_6 Hex.Conway.compat_3_1_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_2_6 :

Hex.GFq 3 2 Hex.Conway.supportedEntry_3_2 →+* Hex.GFq 3 6 Hex.Conway.supportedEntry_3_6

The canonical embedding of GF(3^2) into GF(3^6).

Equations

HexGFqMathlib.Conway.embed_3_2_6 = HexGFqMathlib.conwayEmbed 3 2 6 Hex.Conway.supportedEntry_3_2 Hex.Conway.supportedEntry_3_6 Hex.Conway.compat_3_2_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_3_6 :

Hex.GFq 3 3 Hex.Conway.supportedEntry_3_3 →+* Hex.GFq 3 6 Hex.Conway.supportedEntry_3_6

The canonical embedding of GF(3^3) into GF(3^6).

Equations

HexGFqMathlib.Conway.embed_3_3_6 = HexGFqMathlib.conwayEmbed 3 3 6 Hex.Conway.supportedEntry_3_3 Hex.Conway.supportedEntry_3_6 Hex.Conway.compat_3_3_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_1_7 :

Hex.GFq 3 1 Hex.Conway.supportedEntry_3_1 →+* Hex.GFq 3 7 Hex.Conway.supportedEntry_3_7

The canonical embedding of GF(3^1) into GF(3^7).

Equations

HexGFqMathlib.Conway.embed_3_1_7 = HexGFqMathlib.conwayEmbed 3 1 7 Hex.Conway.supportedEntry_3_1 Hex.Conway.supportedEntry_3_7 Hex.Conway.compat_3_1_7

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_1_8 :

Hex.GFq 3 1 Hex.Conway.supportedEntry_3_1 →+* Hex.GFq 3 8 Hex.Conway.supportedEntry_3_8

The canonical embedding of GF(3^1) into GF(3^8).

Equations

HexGFqMathlib.Conway.embed_3_1_8 = HexGFqMathlib.conwayEmbed 3 1 8 Hex.Conway.supportedEntry_3_1 Hex.Conway.supportedEntry_3_8 Hex.Conway.compat_3_1_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_2_8 :

Hex.GFq 3 2 Hex.Conway.supportedEntry_3_2 →+* Hex.GFq 3 8 Hex.Conway.supportedEntry_3_8

The canonical embedding of GF(3^2) into GF(3^8).

Equations

HexGFqMathlib.Conway.embed_3_2_8 = HexGFqMathlib.conwayEmbed 3 2 8 Hex.Conway.supportedEntry_3_2 Hex.Conway.supportedEntry_3_8 Hex.Conway.compat_3_2_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_3_4_8 :

Hex.GFq 3 4 Hex.Conway.supportedEntry_3_4 →+* Hex.GFq 3 8 Hex.Conway.supportedEntry_3_8

The canonical embedding of GF(3^4) into GF(3^8).

Equations

HexGFqMathlib.Conway.embed_3_4_8 = HexGFqMathlib.conwayEmbed 3 4 8 Hex.Conway.supportedEntry_3_4 Hex.Conway.supportedEntry_3_8 Hex.Conway.compat_3_4_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_1_2 :

Hex.GFq 5 1 Hex.Conway.supportedEntry_5_1 →+* Hex.GFq 5 2 Hex.Conway.supportedEntry_5_2

The canonical embedding of GF(5^1) into GF(5^2).

Equations

HexGFqMathlib.Conway.embed_5_1_2 = HexGFqMathlib.conwayEmbed 5 1 2 Hex.Conway.supportedEntry_5_1 Hex.Conway.supportedEntry_5_2 Hex.Conway.compat_5_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_1_3 :

Hex.GFq 5 1 Hex.Conway.supportedEntry_5_1 →+* Hex.GFq 5 3 Hex.Conway.supportedEntry_5_3

The canonical embedding of GF(5^1) into GF(5^3).

Equations

HexGFqMathlib.Conway.embed_5_1_3 = HexGFqMathlib.conwayEmbed 5 1 3 Hex.Conway.supportedEntry_5_1 Hex.Conway.supportedEntry_5_3 Hex.Conway.compat_5_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_1_4 :

Hex.GFq 5 1 Hex.Conway.supportedEntry_5_1 →+* Hex.GFq 5 4 Hex.Conway.supportedEntry_5_4

The canonical embedding of GF(5^1) into GF(5^4).

Equations

HexGFqMathlib.Conway.embed_5_1_4 = HexGFqMathlib.conwayEmbed 5 1 4 Hex.Conway.supportedEntry_5_1 Hex.Conway.supportedEntry_5_4 Hex.Conway.compat_5_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_2_4 :

Hex.GFq 5 2 Hex.Conway.supportedEntry_5_2 →+* Hex.GFq 5 4 Hex.Conway.supportedEntry_5_4

The canonical embedding of GF(5^2) into GF(5^4).

Equations

HexGFqMathlib.Conway.embed_5_2_4 = HexGFqMathlib.conwayEmbed 5 2 4 Hex.Conway.supportedEntry_5_2 Hex.Conway.supportedEntry_5_4 Hex.Conway.compat_5_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_1_5 :

Hex.GFq 5 1 Hex.Conway.supportedEntry_5_1 →+* Hex.GFq 5 5 Hex.Conway.supportedEntry_5_5

The canonical embedding of GF(5^1) into GF(5^5).

Equations

HexGFqMathlib.Conway.embed_5_1_5 = HexGFqMathlib.conwayEmbed 5 1 5 Hex.Conway.supportedEntry_5_1 Hex.Conway.supportedEntry_5_5 Hex.Conway.compat_5_1_5

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_1_6 :

Hex.GFq 5 1 Hex.Conway.supportedEntry_5_1 →+* Hex.GFq 5 6 Hex.Conway.supportedEntry_5_6

The canonical embedding of GF(5^1) into GF(5^6).

Equations

HexGFqMathlib.Conway.embed_5_1_6 = HexGFqMathlib.conwayEmbed 5 1 6 Hex.Conway.supportedEntry_5_1 Hex.Conway.supportedEntry_5_6 Hex.Conway.compat_5_1_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_2_6 :

Hex.GFq 5 2 Hex.Conway.supportedEntry_5_2 →+* Hex.GFq 5 6 Hex.Conway.supportedEntry_5_6

The canonical embedding of GF(5^2) into GF(5^6).

Equations

HexGFqMathlib.Conway.embed_5_2_6 = HexGFqMathlib.conwayEmbed 5 2 6 Hex.Conway.supportedEntry_5_2 Hex.Conway.supportedEntry_5_6 Hex.Conway.compat_5_2_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_3_6 :

Hex.GFq 5 3 Hex.Conway.supportedEntry_5_3 →+* Hex.GFq 5 6 Hex.Conway.supportedEntry_5_6

The canonical embedding of GF(5^3) into GF(5^6).

Equations

HexGFqMathlib.Conway.embed_5_3_6 = HexGFqMathlib.conwayEmbed 5 3 6 Hex.Conway.supportedEntry_5_3 Hex.Conway.supportedEntry_5_6 Hex.Conway.compat_5_3_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_1_7 :

Hex.GFq 5 1 Hex.Conway.supportedEntry_5_1 →+* Hex.GFq 5 7 Hex.Conway.supportedEntry_5_7

The canonical embedding of GF(5^1) into GF(5^7).

Equations

HexGFqMathlib.Conway.embed_5_1_7 = HexGFqMathlib.conwayEmbed 5 1 7 Hex.Conway.supportedEntry_5_1 Hex.Conway.supportedEntry_5_7 Hex.Conway.compat_5_1_7

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_1_8 :

Hex.GFq 5 1 Hex.Conway.supportedEntry_5_1 →+* Hex.GFq 5 8 Hex.Conway.supportedEntry_5_8

The canonical embedding of GF(5^1) into GF(5^8).

Equations

HexGFqMathlib.Conway.embed_5_1_8 = HexGFqMathlib.conwayEmbed 5 1 8 Hex.Conway.supportedEntry_5_1 Hex.Conway.supportedEntry_5_8 Hex.Conway.compat_5_1_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_2_8 :

Hex.GFq 5 2 Hex.Conway.supportedEntry_5_2 →+* Hex.GFq 5 8 Hex.Conway.supportedEntry_5_8

The canonical embedding of GF(5^2) into GF(5^8).

Equations

HexGFqMathlib.Conway.embed_5_2_8 = HexGFqMathlib.conwayEmbed 5 2 8 Hex.Conway.supportedEntry_5_2 Hex.Conway.supportedEntry_5_8 Hex.Conway.compat_5_2_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_5_4_8 :

Hex.GFq 5 4 Hex.Conway.supportedEntry_5_4 →+* Hex.GFq 5 8 Hex.Conway.supportedEntry_5_8

The canonical embedding of GF(5^4) into GF(5^8).

Equations

HexGFqMathlib.Conway.embed_5_4_8 = HexGFqMathlib.conwayEmbed 5 4 8 Hex.Conway.supportedEntry_5_4 Hex.Conway.supportedEntry_5_8 Hex.Conway.compat_5_4_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_1_2 :

Hex.GFq 7 1 Hex.Conway.supportedEntry_7_1 →+* Hex.GFq 7 2 Hex.Conway.supportedEntry_7_2

The canonical embedding of GF(7^1) into GF(7^2).

Equations

HexGFqMathlib.Conway.embed_7_1_2 = HexGFqMathlib.conwayEmbed 7 1 2 Hex.Conway.supportedEntry_7_1 Hex.Conway.supportedEntry_7_2 Hex.Conway.compat_7_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_1_3 :

Hex.GFq 7 1 Hex.Conway.supportedEntry_7_1 →+* Hex.GFq 7 3 Hex.Conway.supportedEntry_7_3

The canonical embedding of GF(7^1) into GF(7^3).

Equations

HexGFqMathlib.Conway.embed_7_1_3 = HexGFqMathlib.conwayEmbed 7 1 3 Hex.Conway.supportedEntry_7_1 Hex.Conway.supportedEntry_7_3 Hex.Conway.compat_7_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_1_4 :

Hex.GFq 7 1 Hex.Conway.supportedEntry_7_1 →+* Hex.GFq 7 4 Hex.Conway.supportedEntry_7_4

The canonical embedding of GF(7^1) into GF(7^4).

Equations

HexGFqMathlib.Conway.embed_7_1_4 = HexGFqMathlib.conwayEmbed 7 1 4 Hex.Conway.supportedEntry_7_1 Hex.Conway.supportedEntry_7_4 Hex.Conway.compat_7_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_2_4 :

Hex.GFq 7 2 Hex.Conway.supportedEntry_7_2 →+* Hex.GFq 7 4 Hex.Conway.supportedEntry_7_4

The canonical embedding of GF(7^2) into GF(7^4).

Equations

HexGFqMathlib.Conway.embed_7_2_4 = HexGFqMathlib.conwayEmbed 7 2 4 Hex.Conway.supportedEntry_7_2 Hex.Conway.supportedEntry_7_4 Hex.Conway.compat_7_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_1_5 :

Hex.GFq 7 1 Hex.Conway.supportedEntry_7_1 →+* Hex.GFq 7 5 Hex.Conway.supportedEntry_7_5

The canonical embedding of GF(7^1) into GF(7^5).

Equations

HexGFqMathlib.Conway.embed_7_1_5 = HexGFqMathlib.conwayEmbed 7 1 5 Hex.Conway.supportedEntry_7_1 Hex.Conway.supportedEntry_7_5 Hex.Conway.compat_7_1_5

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_1_6 :

Hex.GFq 7 1 Hex.Conway.supportedEntry_7_1 →+* Hex.GFq 7 6 Hex.Conway.supportedEntry_7_6

The canonical embedding of GF(7^1) into GF(7^6).

Equations

HexGFqMathlib.Conway.embed_7_1_6 = HexGFqMathlib.conwayEmbed 7 1 6 Hex.Conway.supportedEntry_7_1 Hex.Conway.supportedEntry_7_6 Hex.Conway.compat_7_1_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_2_6 :

Hex.GFq 7 2 Hex.Conway.supportedEntry_7_2 →+* Hex.GFq 7 6 Hex.Conway.supportedEntry_7_6

The canonical embedding of GF(7^2) into GF(7^6).

Equations

HexGFqMathlib.Conway.embed_7_2_6 = HexGFqMathlib.conwayEmbed 7 2 6 Hex.Conway.supportedEntry_7_2 Hex.Conway.supportedEntry_7_6 Hex.Conway.compat_7_2_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_3_6 :

Hex.GFq 7 3 Hex.Conway.supportedEntry_7_3 →+* Hex.GFq 7 6 Hex.Conway.supportedEntry_7_6

The canonical embedding of GF(7^3) into GF(7^6).

Equations

HexGFqMathlib.Conway.embed_7_3_6 = HexGFqMathlib.conwayEmbed 7 3 6 Hex.Conway.supportedEntry_7_3 Hex.Conway.supportedEntry_7_6 Hex.Conway.compat_7_3_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_1_7 :

Hex.GFq 7 1 Hex.Conway.supportedEntry_7_1 →+* Hex.GFq 7 7 Hex.Conway.supportedEntry_7_7

The canonical embedding of GF(7^1) into GF(7^7).

Equations

HexGFqMathlib.Conway.embed_7_1_7 = HexGFqMathlib.conwayEmbed 7 1 7 Hex.Conway.supportedEntry_7_1 Hex.Conway.supportedEntry_7_7 Hex.Conway.compat_7_1_7

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_1_8 :

Hex.GFq 7 1 Hex.Conway.supportedEntry_7_1 →+* Hex.GFq 7 8 Hex.Conway.supportedEntry_7_8

The canonical embedding of GF(7^1) into GF(7^8).

Equations

HexGFqMathlib.Conway.embed_7_1_8 = HexGFqMathlib.conwayEmbed 7 1 8 Hex.Conway.supportedEntry_7_1 Hex.Conway.supportedEntry_7_8 Hex.Conway.compat_7_1_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_2_8 :

Hex.GFq 7 2 Hex.Conway.supportedEntry_7_2 →+* Hex.GFq 7 8 Hex.Conway.supportedEntry_7_8

The canonical embedding of GF(7^2) into GF(7^8).

Equations

HexGFqMathlib.Conway.embed_7_2_8 = HexGFqMathlib.conwayEmbed 7 2 8 Hex.Conway.supportedEntry_7_2 Hex.Conway.supportedEntry_7_8 Hex.Conway.compat_7_2_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_7_4_8 :

Hex.GFq 7 4 Hex.Conway.supportedEntry_7_4 →+* Hex.GFq 7 8 Hex.Conway.supportedEntry_7_8

The canonical embedding of GF(7^4) into GF(7^8).

Equations

HexGFqMathlib.Conway.embed_7_4_8 = HexGFqMathlib.conwayEmbed 7 4 8 Hex.Conway.supportedEntry_7_4 Hex.Conway.supportedEntry_7_8 Hex.Conway.compat_7_4_8

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_11_1_2 :

Hex.GFq 11 1 Hex.Conway.supportedEntry_11_1 →+* Hex.GFq 11 2 Hex.Conway.supportedEntry_11_2

The canonical embedding of GF(11^1) into GF(11^2).

Equations

HexGFqMathlib.Conway.embed_11_1_2 = HexGFqMathlib.conwayEmbed 11 1 2 Hex.Conway.supportedEntry_11_1 Hex.Conway.supportedEntry_11_2 Hex.Conway.compat_11_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_11_1_3 :

Hex.GFq 11 1 Hex.Conway.supportedEntry_11_1 →+* Hex.GFq 11 3 Hex.Conway.supportedEntry_11_3

The canonical embedding of GF(11^1) into GF(11^3).

Equations

HexGFqMathlib.Conway.embed_11_1_3 = HexGFqMathlib.conwayEmbed 11 1 3 Hex.Conway.supportedEntry_11_1 Hex.Conway.supportedEntry_11_3 Hex.Conway.compat_11_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_11_1_4 :

Hex.GFq 11 1 Hex.Conway.supportedEntry_11_1 →+* Hex.GFq 11 4 Hex.Conway.supportedEntry_11_4

The canonical embedding of GF(11^1) into GF(11^4).

Equations

HexGFqMathlib.Conway.embed_11_1_4 = HexGFqMathlib.conwayEmbed 11 1 4 Hex.Conway.supportedEntry_11_1 Hex.Conway.supportedEntry_11_4 Hex.Conway.compat_11_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_11_2_4 :

Hex.GFq 11 2 Hex.Conway.supportedEntry_11_2 →+* Hex.GFq 11 4 Hex.Conway.supportedEntry_11_4

The canonical embedding of GF(11^2) into GF(11^4).

Equations

HexGFqMathlib.Conway.embed_11_2_4 = HexGFqMathlib.conwayEmbed 11 2 4 Hex.Conway.supportedEntry_11_2 Hex.Conway.supportedEntry_11_4 Hex.Conway.compat_11_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_11_1_5 :

Hex.GFq 11 1 Hex.Conway.supportedEntry_11_1 →+* Hex.GFq 11 5 Hex.Conway.supportedEntry_11_5

The canonical embedding of GF(11^1) into GF(11^5).

Equations

HexGFqMathlib.Conway.embed_11_1_5 = HexGFqMathlib.conwayEmbed 11 1 5 Hex.Conway.supportedEntry_11_1 Hex.Conway.supportedEntry_11_5 Hex.Conway.compat_11_1_5

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_11_1_6 :

Hex.GFq 11 1 Hex.Conway.supportedEntry_11_1 →+* Hex.GFq 11 6 Hex.Conway.supportedEntry_11_6

The canonical embedding of GF(11^1) into GF(11^6).

Equations

HexGFqMathlib.Conway.embed_11_1_6 = HexGFqMathlib.conwayEmbed 11 1 6 Hex.Conway.supportedEntry_11_1 Hex.Conway.supportedEntry_11_6 Hex.Conway.compat_11_1_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_11_2_6 :

Hex.GFq 11 2 Hex.Conway.supportedEntry_11_2 →+* Hex.GFq 11 6 Hex.Conway.supportedEntry_11_6

The canonical embedding of GF(11^2) into GF(11^6).

Equations

HexGFqMathlib.Conway.embed_11_2_6 = HexGFqMathlib.conwayEmbed 11 2 6 Hex.Conway.supportedEntry_11_2 Hex.Conway.supportedEntry_11_6 Hex.Conway.compat_11_2_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_11_3_6 :

Hex.GFq 11 3 Hex.Conway.supportedEntry_11_3 →+* Hex.GFq 11 6 Hex.Conway.supportedEntry_11_6

The canonical embedding of GF(11^3) into GF(11^6).

Equations

HexGFqMathlib.Conway.embed_11_3_6 = HexGFqMathlib.conwayEmbed 11 3 6 Hex.Conway.supportedEntry_11_3 Hex.Conway.supportedEntry_11_6 Hex.Conway.compat_11_3_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_13_1_2 :

Hex.GFq 13 1 Hex.Conway.supportedEntry_13_1 →+* Hex.GFq 13 2 Hex.Conway.supportedEntry_13_2

The canonical embedding of GF(13^1) into GF(13^2).

Equations

HexGFqMathlib.Conway.embed_13_1_2 = HexGFqMathlib.conwayEmbed 13 1 2 Hex.Conway.supportedEntry_13_1 Hex.Conway.supportedEntry_13_2 Hex.Conway.compat_13_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_13_1_3 :

Hex.GFq 13 1 Hex.Conway.supportedEntry_13_1 →+* Hex.GFq 13 3 Hex.Conway.supportedEntry_13_3

The canonical embedding of GF(13^1) into GF(13^3).

Equations

HexGFqMathlib.Conway.embed_13_1_3 = HexGFqMathlib.conwayEmbed 13 1 3 Hex.Conway.supportedEntry_13_1 Hex.Conway.supportedEntry_13_3 Hex.Conway.compat_13_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_13_1_4 :

Hex.GFq 13 1 Hex.Conway.supportedEntry_13_1 →+* Hex.GFq 13 4 Hex.Conway.supportedEntry_13_4

The canonical embedding of GF(13^1) into GF(13^4).

Equations

HexGFqMathlib.Conway.embed_13_1_4 = HexGFqMathlib.conwayEmbed 13 1 4 Hex.Conway.supportedEntry_13_1 Hex.Conway.supportedEntry_13_4 Hex.Conway.compat_13_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_13_2_4 :

Hex.GFq 13 2 Hex.Conway.supportedEntry_13_2 →+* Hex.GFq 13 4 Hex.Conway.supportedEntry_13_4

The canonical embedding of GF(13^2) into GF(13^4).

Equations

HexGFqMathlib.Conway.embed_13_2_4 = HexGFqMathlib.conwayEmbed 13 2 4 Hex.Conway.supportedEntry_13_2 Hex.Conway.supportedEntry_13_4 Hex.Conway.compat_13_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_13_1_5 :

Hex.GFq 13 1 Hex.Conway.supportedEntry_13_1 →+* Hex.GFq 13 5 Hex.Conway.supportedEntry_13_5

The canonical embedding of GF(13^1) into GF(13^5).

Equations

HexGFqMathlib.Conway.embed_13_1_5 = HexGFqMathlib.conwayEmbed 13 1 5 Hex.Conway.supportedEntry_13_1 Hex.Conway.supportedEntry_13_5 Hex.Conway.compat_13_1_5

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_13_1_6 :

Hex.GFq 13 1 Hex.Conway.supportedEntry_13_1 →+* Hex.GFq 13 6 Hex.Conway.supportedEntry_13_6

The canonical embedding of GF(13^1) into GF(13^6).

Equations

HexGFqMathlib.Conway.embed_13_1_6 = HexGFqMathlib.conwayEmbed 13 1 6 Hex.Conway.supportedEntry_13_1 Hex.Conway.supportedEntry_13_6 Hex.Conway.compat_13_1_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_13_2_6 :

Hex.GFq 13 2 Hex.Conway.supportedEntry_13_2 →+* Hex.GFq 13 6 Hex.Conway.supportedEntry_13_6

The canonical embedding of GF(13^2) into GF(13^6).

Equations

HexGFqMathlib.Conway.embed_13_2_6 = HexGFqMathlib.conwayEmbed 13 2 6 Hex.Conway.supportedEntry_13_2 Hex.Conway.supportedEntry_13_6 Hex.Conway.compat_13_2_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_13_3_6 :

Hex.GFq 13 3 Hex.Conway.supportedEntry_13_3 →+* Hex.GFq 13 6 Hex.Conway.supportedEntry_13_6

The canonical embedding of GF(13^3) into GF(13^6).

Equations

HexGFqMathlib.Conway.embed_13_3_6 = HexGFqMathlib.conwayEmbed 13 3 6 Hex.Conway.supportedEntry_13_3 Hex.Conway.supportedEntry_13_6 Hex.Conway.compat_13_3_6

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_17_1_2 :

Hex.GFq 17 1 Hex.Conway.supportedEntry_17_1 →+* Hex.GFq 17 2 Hex.Conway.supportedEntry_17_2

The canonical embedding of GF(17^1) into GF(17^2).

Equations

HexGFqMathlib.Conway.embed_17_1_2 = HexGFqMathlib.conwayEmbed 17 1 2 Hex.Conway.supportedEntry_17_1 Hex.Conway.supportedEntry_17_2 Hex.Conway.compat_17_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_17_1_3 :

Hex.GFq 17 1 Hex.Conway.supportedEntry_17_1 →+* Hex.GFq 17 3 Hex.Conway.supportedEntry_17_3

The canonical embedding of GF(17^1) into GF(17^3).

Equations

HexGFqMathlib.Conway.embed_17_1_3 = HexGFqMathlib.conwayEmbed 17 1 3 Hex.Conway.supportedEntry_17_1 Hex.Conway.supportedEntry_17_3 Hex.Conway.compat_17_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_17_1_4 :

Hex.GFq 17 1 Hex.Conway.supportedEntry_17_1 →+* Hex.GFq 17 4 Hex.Conway.supportedEntry_17_4

The canonical embedding of GF(17^1) into GF(17^4).

Equations

HexGFqMathlib.Conway.embed_17_1_4 = HexGFqMathlib.conwayEmbed 17 1 4 Hex.Conway.supportedEntry_17_1 Hex.Conway.supportedEntry_17_4 Hex.Conway.compat_17_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_17_2_4 :

Hex.GFq 17 2 Hex.Conway.supportedEntry_17_2 →+* Hex.GFq 17 4 Hex.Conway.supportedEntry_17_4

The canonical embedding of GF(17^2) into GF(17^4).

Equations

HexGFqMathlib.Conway.embed_17_2_4 = HexGFqMathlib.conwayEmbed 17 2 4 Hex.Conway.supportedEntry_17_2 Hex.Conway.supportedEntry_17_4 Hex.Conway.compat_17_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_19_1_2 :

Hex.GFq 19 1 Hex.Conway.supportedEntry_19_1 →+* Hex.GFq 19 2 Hex.Conway.supportedEntry_19_2

The canonical embedding of GF(19^1) into GF(19^2).

Equations

HexGFqMathlib.Conway.embed_19_1_2 = HexGFqMathlib.conwayEmbed 19 1 2 Hex.Conway.supportedEntry_19_1 Hex.Conway.supportedEntry_19_2 Hex.Conway.compat_19_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_19_1_3 :

Hex.GFq 19 1 Hex.Conway.supportedEntry_19_1 →+* Hex.GFq 19 3 Hex.Conway.supportedEntry_19_3

The canonical embedding of GF(19^1) into GF(19^3).

Equations

HexGFqMathlib.Conway.embed_19_1_3 = HexGFqMathlib.conwayEmbed 19 1 3 Hex.Conway.supportedEntry_19_1 Hex.Conway.supportedEntry_19_3 Hex.Conway.compat_19_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_19_1_4 :

Hex.GFq 19 1 Hex.Conway.supportedEntry_19_1 →+* Hex.GFq 19 4 Hex.Conway.supportedEntry_19_4

The canonical embedding of GF(19^1) into GF(19^4).

Equations

HexGFqMathlib.Conway.embed_19_1_4 = HexGFqMathlib.conwayEmbed 19 1 4 Hex.Conway.supportedEntry_19_1 Hex.Conway.supportedEntry_19_4 Hex.Conway.compat_19_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_19_2_4 :

Hex.GFq 19 2 Hex.Conway.supportedEntry_19_2 →+* Hex.GFq 19 4 Hex.Conway.supportedEntry_19_4

The canonical embedding of GF(19^2) into GF(19^4).

Equations

HexGFqMathlib.Conway.embed_19_2_4 = HexGFqMathlib.conwayEmbed 19 2 4 Hex.Conway.supportedEntry_19_2 Hex.Conway.supportedEntry_19_4 Hex.Conway.compat_19_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_23_1_2 :

Hex.GFq 23 1 Hex.Conway.supportedEntry_23_1 →+* Hex.GFq 23 2 Hex.Conway.supportedEntry_23_2

The canonical embedding of GF(23^1) into GF(23^2).

Equations

HexGFqMathlib.Conway.embed_23_1_2 = HexGFqMathlib.conwayEmbed 23 1 2 Hex.Conway.supportedEntry_23_1 Hex.Conway.supportedEntry_23_2 Hex.Conway.compat_23_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_23_1_3 :

Hex.GFq 23 1 Hex.Conway.supportedEntry_23_1 →+* Hex.GFq 23 3 Hex.Conway.supportedEntry_23_3

The canonical embedding of GF(23^1) into GF(23^3).

Equations

HexGFqMathlib.Conway.embed_23_1_3 = HexGFqMathlib.conwayEmbed 23 1 3 Hex.Conway.supportedEntry_23_1 Hex.Conway.supportedEntry_23_3 Hex.Conway.compat_23_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_23_1_4 :

Hex.GFq 23 1 Hex.Conway.supportedEntry_23_1 →+* Hex.GFq 23 4 Hex.Conway.supportedEntry_23_4

The canonical embedding of GF(23^1) into GF(23^4).

Equations

HexGFqMathlib.Conway.embed_23_1_4 = HexGFqMathlib.conwayEmbed 23 1 4 Hex.Conway.supportedEntry_23_1 Hex.Conway.supportedEntry_23_4 Hex.Conway.compat_23_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_23_2_4 :

Hex.GFq 23 2 Hex.Conway.supportedEntry_23_2 →+* Hex.GFq 23 4 Hex.Conway.supportedEntry_23_4

The canonical embedding of GF(23^2) into GF(23^4).

Equations

HexGFqMathlib.Conway.embed_23_2_4 = HexGFqMathlib.conwayEmbed 23 2 4 Hex.Conway.supportedEntry_23_2 Hex.Conway.supportedEntry_23_4 Hex.Conway.compat_23_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_29_1_2 :

Hex.GFq 29 1 Hex.Conway.supportedEntry_29_1 →+* Hex.GFq 29 2 Hex.Conway.supportedEntry_29_2

The canonical embedding of GF(29^1) into GF(29^2).

Equations

HexGFqMathlib.Conway.embed_29_1_2 = HexGFqMathlib.conwayEmbed 29 1 2 Hex.Conway.supportedEntry_29_1 Hex.Conway.supportedEntry_29_2 Hex.Conway.compat_29_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_29_1_3 :

Hex.GFq 29 1 Hex.Conway.supportedEntry_29_1 →+* Hex.GFq 29 3 Hex.Conway.supportedEntry_29_3

The canonical embedding of GF(29^1) into GF(29^3).

Equations

HexGFqMathlib.Conway.embed_29_1_3 = HexGFqMathlib.conwayEmbed 29 1 3 Hex.Conway.supportedEntry_29_1 Hex.Conway.supportedEntry_29_3 Hex.Conway.compat_29_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_29_1_4 :

Hex.GFq 29 1 Hex.Conway.supportedEntry_29_1 →+* Hex.GFq 29 4 Hex.Conway.supportedEntry_29_4

The canonical embedding of GF(29^1) into GF(29^4).

Equations

HexGFqMathlib.Conway.embed_29_1_4 = HexGFqMathlib.conwayEmbed 29 1 4 Hex.Conway.supportedEntry_29_1 Hex.Conway.supportedEntry_29_4 Hex.Conway.compat_29_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_29_2_4 :

Hex.GFq 29 2 Hex.Conway.supportedEntry_29_2 →+* Hex.GFq 29 4 Hex.Conway.supportedEntry_29_4

The canonical embedding of GF(29^2) into GF(29^4).

Equations

HexGFqMathlib.Conway.embed_29_2_4 = HexGFqMathlib.conwayEmbed 29 2 4 Hex.Conway.supportedEntry_29_2 Hex.Conway.supportedEntry_29_4 Hex.Conway.compat_29_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_31_1_2 :

Hex.GFq 31 1 Hex.Conway.supportedEntry_31_1 →+* Hex.GFq 31 2 Hex.Conway.supportedEntry_31_2

The canonical embedding of GF(31^1) into GF(31^2).

Equations

HexGFqMathlib.Conway.embed_31_1_2 = HexGFqMathlib.conwayEmbed 31 1 2 Hex.Conway.supportedEntry_31_1 Hex.Conway.supportedEntry_31_2 Hex.Conway.compat_31_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_31_1_3 :

Hex.GFq 31 1 Hex.Conway.supportedEntry_31_1 →+* Hex.GFq 31 3 Hex.Conway.supportedEntry_31_3

The canonical embedding of GF(31^1) into GF(31^3).

Equations

HexGFqMathlib.Conway.embed_31_1_3 = HexGFqMathlib.conwayEmbed 31 1 3 Hex.Conway.supportedEntry_31_1 Hex.Conway.supportedEntry_31_3 Hex.Conway.compat_31_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_31_1_4 :

Hex.GFq 31 1 Hex.Conway.supportedEntry_31_1 →+* Hex.GFq 31 4 Hex.Conway.supportedEntry_31_4

The canonical embedding of GF(31^1) into GF(31^4).

Equations

HexGFqMathlib.Conway.embed_31_1_4 = HexGFqMathlib.conwayEmbed 31 1 4 Hex.Conway.supportedEntry_31_1 Hex.Conway.supportedEntry_31_4 Hex.Conway.compat_31_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_31_2_4 :

Hex.GFq 31 2 Hex.Conway.supportedEntry_31_2 →+* Hex.GFq 31 4 Hex.Conway.supportedEntry_31_4

The canonical embedding of GF(31^2) into GF(31^4).

Equations

HexGFqMathlib.Conway.embed_31_2_4 = HexGFqMathlib.conwayEmbed 31 2 4 Hex.Conway.supportedEntry_31_2 Hex.Conway.supportedEntry_31_4 Hex.Conway.compat_31_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_37_1_2 :

Hex.GFq 37 1 Hex.Conway.supportedEntry_37_1 →+* Hex.GFq 37 2 Hex.Conway.supportedEntry_37_2

The canonical embedding of GF(37^1) into GF(37^2).

Equations

HexGFqMathlib.Conway.embed_37_1_2 = HexGFqMathlib.conwayEmbed 37 1 2 Hex.Conway.supportedEntry_37_1 Hex.Conway.supportedEntry_37_2 Hex.Conway.compat_37_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_37_1_3 :

Hex.GFq 37 1 Hex.Conway.supportedEntry_37_1 →+* Hex.GFq 37 3 Hex.Conway.supportedEntry_37_3

The canonical embedding of GF(37^1) into GF(37^3).

Equations

HexGFqMathlib.Conway.embed_37_1_3 = HexGFqMathlib.conwayEmbed 37 1 3 Hex.Conway.supportedEntry_37_1 Hex.Conway.supportedEntry_37_3 Hex.Conway.compat_37_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_37_1_4 :

Hex.GFq 37 1 Hex.Conway.supportedEntry_37_1 →+* Hex.GFq 37 4 Hex.Conway.supportedEntry_37_4

The canonical embedding of GF(37^1) into GF(37^4).

Equations

HexGFqMathlib.Conway.embed_37_1_4 = HexGFqMathlib.conwayEmbed 37 1 4 Hex.Conway.supportedEntry_37_1 Hex.Conway.supportedEntry_37_4 Hex.Conway.compat_37_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_37_2_4 :

Hex.GFq 37 2 Hex.Conway.supportedEntry_37_2 →+* Hex.GFq 37 4 Hex.Conway.supportedEntry_37_4

The canonical embedding of GF(37^2) into GF(37^4).

Equations

HexGFqMathlib.Conway.embed_37_2_4 = HexGFqMathlib.conwayEmbed 37 2 4 Hex.Conway.supportedEntry_37_2 Hex.Conway.supportedEntry_37_4 Hex.Conway.compat_37_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_41_1_2 :

Hex.GFq 41 1 Hex.Conway.supportedEntry_41_1 →+* Hex.GFq 41 2 Hex.Conway.supportedEntry_41_2

The canonical embedding of GF(41^1) into GF(41^2).

Equations

HexGFqMathlib.Conway.embed_41_1_2 = HexGFqMathlib.conwayEmbed 41 1 2 Hex.Conway.supportedEntry_41_1 Hex.Conway.supportedEntry_41_2 Hex.Conway.compat_41_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_41_1_3 :

Hex.GFq 41 1 Hex.Conway.supportedEntry_41_1 →+* Hex.GFq 41 3 Hex.Conway.supportedEntry_41_3

The canonical embedding of GF(41^1) into GF(41^3).

Equations

HexGFqMathlib.Conway.embed_41_1_3 = HexGFqMathlib.conwayEmbed 41 1 3 Hex.Conway.supportedEntry_41_1 Hex.Conway.supportedEntry_41_3 Hex.Conway.compat_41_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_41_1_4 :

Hex.GFq 41 1 Hex.Conway.supportedEntry_41_1 →+* Hex.GFq 41 4 Hex.Conway.supportedEntry_41_4

The canonical embedding of GF(41^1) into GF(41^4).

Equations

HexGFqMathlib.Conway.embed_41_1_4 = HexGFqMathlib.conwayEmbed 41 1 4 Hex.Conway.supportedEntry_41_1 Hex.Conway.supportedEntry_41_4 Hex.Conway.compat_41_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_41_2_4 :

Hex.GFq 41 2 Hex.Conway.supportedEntry_41_2 →+* Hex.GFq 41 4 Hex.Conway.supportedEntry_41_4

The canonical embedding of GF(41^2) into GF(41^4).

Equations

HexGFqMathlib.Conway.embed_41_2_4 = HexGFqMathlib.conwayEmbed 41 2 4 Hex.Conway.supportedEntry_41_2 Hex.Conway.supportedEntry_41_4 Hex.Conway.compat_41_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_43_1_2 :

Hex.GFq 43 1 Hex.Conway.supportedEntry_43_1 →+* Hex.GFq 43 2 Hex.Conway.supportedEntry_43_2

The canonical embedding of GF(43^1) into GF(43^2).

Equations

HexGFqMathlib.Conway.embed_43_1_2 = HexGFqMathlib.conwayEmbed 43 1 2 Hex.Conway.supportedEntry_43_1 Hex.Conway.supportedEntry_43_2 Hex.Conway.compat_43_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_43_1_3 :

Hex.GFq 43 1 Hex.Conway.supportedEntry_43_1 →+* Hex.GFq 43 3 Hex.Conway.supportedEntry_43_3

The canonical embedding of GF(43^1) into GF(43^3).

Equations

HexGFqMathlib.Conway.embed_43_1_3 = HexGFqMathlib.conwayEmbed 43 1 3 Hex.Conway.supportedEntry_43_1 Hex.Conway.supportedEntry_43_3 Hex.Conway.compat_43_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_43_1_4 :

Hex.GFq 43 1 Hex.Conway.supportedEntry_43_1 →+* Hex.GFq 43 4 Hex.Conway.supportedEntry_43_4

The canonical embedding of GF(43^1) into GF(43^4).

Equations

HexGFqMathlib.Conway.embed_43_1_4 = HexGFqMathlib.conwayEmbed 43 1 4 Hex.Conway.supportedEntry_43_1 Hex.Conway.supportedEntry_43_4 Hex.Conway.compat_43_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_43_2_4 :

Hex.GFq 43 2 Hex.Conway.supportedEntry_43_2 →+* Hex.GFq 43 4 Hex.Conway.supportedEntry_43_4

The canonical embedding of GF(43^2) into GF(43^4).

Equations

HexGFqMathlib.Conway.embed_43_2_4 = HexGFqMathlib.conwayEmbed 43 2 4 Hex.Conway.supportedEntry_43_2 Hex.Conway.supportedEntry_43_4 Hex.Conway.compat_43_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_47_1_2 :

Hex.GFq 47 1 Hex.Conway.supportedEntry_47_1 →+* Hex.GFq 47 2 Hex.Conway.supportedEntry_47_2

The canonical embedding of GF(47^1) into GF(47^2).

Equations

HexGFqMathlib.Conway.embed_47_1_2 = HexGFqMathlib.conwayEmbed 47 1 2 Hex.Conway.supportedEntry_47_1 Hex.Conway.supportedEntry_47_2 Hex.Conway.compat_47_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_47_1_3 :

Hex.GFq 47 1 Hex.Conway.supportedEntry_47_1 →+* Hex.GFq 47 3 Hex.Conway.supportedEntry_47_3

The canonical embedding of GF(47^1) into GF(47^3).

Equations

HexGFqMathlib.Conway.embed_47_1_3 = HexGFqMathlib.conwayEmbed 47 1 3 Hex.Conway.supportedEntry_47_1 Hex.Conway.supportedEntry_47_3 Hex.Conway.compat_47_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_47_1_4 :

Hex.GFq 47 1 Hex.Conway.supportedEntry_47_1 →+* Hex.GFq 47 4 Hex.Conway.supportedEntry_47_4

The canonical embedding of GF(47^1) into GF(47^4).

Equations

HexGFqMathlib.Conway.embed_47_1_4 = HexGFqMathlib.conwayEmbed 47 1 4 Hex.Conway.supportedEntry_47_1 Hex.Conway.supportedEntry_47_4 Hex.Conway.compat_47_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_47_2_4 :

Hex.GFq 47 2 Hex.Conway.supportedEntry_47_2 →+* Hex.GFq 47 4 Hex.Conway.supportedEntry_47_4

The canonical embedding of GF(47^2) into GF(47^4).

Equations

HexGFqMathlib.Conway.embed_47_2_4 = HexGFqMathlib.conwayEmbed 47 2 4 Hex.Conway.supportedEntry_47_2 Hex.Conway.supportedEntry_47_4 Hex.Conway.compat_47_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_53_1_2 :

Hex.GFq 53 1 Hex.Conway.supportedEntry_53_1 →+* Hex.GFq 53 2 Hex.Conway.supportedEntry_53_2

The canonical embedding of GF(53^1) into GF(53^2).

Equations

HexGFqMathlib.Conway.embed_53_1_2 = HexGFqMathlib.conwayEmbed 53 1 2 Hex.Conway.supportedEntry_53_1 Hex.Conway.supportedEntry_53_2 Hex.Conway.compat_53_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_53_1_3 :

Hex.GFq 53 1 Hex.Conway.supportedEntry_53_1 →+* Hex.GFq 53 3 Hex.Conway.supportedEntry_53_3

The canonical embedding of GF(53^1) into GF(53^3).

Equations

HexGFqMathlib.Conway.embed_53_1_3 = HexGFqMathlib.conwayEmbed 53 1 3 Hex.Conway.supportedEntry_53_1 Hex.Conway.supportedEntry_53_3 Hex.Conway.compat_53_1_3

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_53_1_4 :

Hex.GFq 53 1 Hex.Conway.supportedEntry_53_1 →+* Hex.GFq 53 4 Hex.Conway.supportedEntry_53_4

The canonical embedding of GF(53^1) into GF(53^4).

Equations

HexGFqMathlib.Conway.embed_53_1_4 = HexGFqMathlib.conwayEmbed 53 1 4 Hex.Conway.supportedEntry_53_1 Hex.Conway.supportedEntry_53_4 Hex.Conway.compat_53_1_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_53_2_4 :

Hex.GFq 53 2 Hex.Conway.supportedEntry_53_2 →+* Hex.GFq 53 4 Hex.Conway.supportedEntry_53_4

The canonical embedding of GF(53^2) into GF(53^4).

Equations

HexGFqMathlib.Conway.embed_53_2_4 = HexGFqMathlib.conwayEmbed 53 2 4 Hex.Conway.supportedEntry_53_2 Hex.Conway.supportedEntry_53_4 Hex.Conway.compat_53_2_4

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_59_1_2 :

Hex.GFq 59 1 Hex.Conway.supportedEntry_59_1 →+* Hex.GFq 59 2 Hex.Conway.supportedEntry_59_2

The canonical embedding of GF(59^1) into GF(59^2).

Equations

HexGFqMathlib.Conway.embed_59_1_2 = HexGFqMathlib.conwayEmbed 59 1 2 Hex.Conway.supportedEntry_59_1 Hex.Conway.supportedEntry_59_2 Hex.Conway.compat_59_1_2

Instances For

source

noncomputable def HexGFqMathlib.Conway.embed_59_1_3 :

Hex.GFq 59 1 Hex.Conway.supportedEntry_59_1 →+* Hex.GFq 59 3 Hex.Conway.supportedEntry_59_3

The canonical embedding of GF(59^1) into GF(59^3).

Equations

HexGFqMathlib.Conway.embed_59_1_3 = HexGFqMathlib.conwayEmbed 59 1 3 Hex.Conway.supportedEntry_59_1 Hex.Conway.supportedEntry_59_3 Hex.Conway.compat_59_1_3

Instances For