Documentation

IMOSLLean4.Generalization.IMO2012N8.IMO2012N8

IMO 2012 N8 (Generalization) #

Find all finite fields $F$ with the following property: for any $r ∈ F$, there exists $a, b ∈ F$ such that $a^2 + b^5 = r$.

Answer #

Any field of cardinality $q ≠ 11$.

Implementation details #

The condition being asked on $F$ is implemented via the predicate good. For the case $q = 11$ and $q = 31$, we show that good is preserved under field isomorphisms via good.of_RingEquiv, so we just have to check the fields ZMod 11 and ZMod 31. For ZMod 11, we show by computer search that $a^2 + b^5 ≠ 7$ for any $a, b ∈ F$. For ZMod 31, we show that every element of $𝔽_{31}$, other than $22 = 4^2 - 5^5$ and $27 = 1^2 + 6^5$, takes the form $a^2$, $a^2 + 1$, or $a^2 - 6^5$ for some $a ∈ 𝔽_{31}$.

source
def IMOSL.IMO2012N8.good (R : Type u_1) [Add R] [Monoid R] :
Prop

A finite field F is called good if every element of F can be written as a^2 + b^5 for some a, b : F.

This is an auxiliary definition, which is not given in the main file since they aren't as focused on representing elements of F specifically as a^2 + b^5.

Equations
Instances For
    source
    theorem IMOSL.IMO2012N8.good.of_RingEquiv {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (hR : good R) (φ : R ≃+* S) :
    good S

    If two rings, R and S, are isomorphic and R is good, then S is good.

    Classifying good finite fields #

    source
    theorem IMOSL.IMO2012N8.good_of_card_big_enough {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : 40 < Fintype.card F) :
    good F

    A finite field of cardinality q > 40 is good.

    source
    theorem IMOSL.IMO2012N8.exists_eq_pow_n_of_gcd_eq_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (hn : n ≠ 0) (h : n.Coprime (Fintype.card F - 1)) (x : F) :
    ∃ (y : F), y ^ n = x

    If n is coprime with q - 1, then every element of F is an nth power.

    source
    theorem IMOSL.IMO2012N8.good_of_card_mod_2_ne_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ¬2 ∣ Fintype.card F - 1) :
    good F

    A finite field of cardinality q ≢ 1 (mod 2) is good.

    source
    theorem IMOSL.IMO2012N8.good_of_card_mod_5_ne_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ¬5 ∣ Fintype.card F - 1) :
    good F

    A finite field of cardinality q ≢ 1 (mod 5) is good.

    source
    theorem IMOSL.IMO2012N8.good_of_card_mod_10_ne_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ¬10 ∣ Fintype.card F - 1) :
    good F

    A finite field of cardinality q ≢ 1 (mod 10) is good.

    source
    theorem IMOSL.IMO2012N8.ZMod11_is_not_good :
    ¬good (ZMod 11)

    The field ZMod 11 is not good.

    source
    theorem IMOSL.IMO2012N8.not_good_of_card_eq_11 {F : Type u_1} [Field F] [Fintype F] (hF : Fintype.card F = 11) :
    ¬good F

    A field of cardinality 11 is not good.

    source
    theorem IMOSL.IMO2012N8.ZMod31_is_good :
    good (ZMod 31)

    The field ZMod 31 is good.

    source
    theorem IMOSL.IMO2012N8.prime_31 :
    Nat.Prime 31

    The integer 31 is prime.

    source
    theorem IMOSL.IMO2012N8.good_of_card_eq_31 {F : Type u_1} [Field F] [Fintype F] (hF : Fintype.card F = 31) :
    good F

    A field of cardinality 31 is good.

    source
    theorem IMOSL.IMO2012N8.not_IsPrimePow_21 :
    ¬IsPrimePow 21

    The integer 21 is not a prime power.

    source
    theorem IMOSL.IMO2012N8.Generalization.final_solution {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] :
    good F ↔ ¬Fintype.card F = 11

    Final solution to the generalized version