Documentation

IMOSLLean4.Generalization.IMO2012A5.Extra.ExplicitRings.F3

Explicit construction of 𝔽₃ #

In this file, we explicitly construct 𝔽₃, the field of 3 elements. We prove that it is a ring, and we construct ring homomorphisms from 𝔽₃.

source
inductive IMOSL.IMO2012A5.Generalization.𝔽₃ :
Type
Instances For
    source
    def IMOSL.IMO2012A5.Generalization.𝔽₃.add :
    𝔽₃ → 𝔽₃ → 𝔽₃
    Equations
    Instances For
      source
      def IMOSL.IMO2012A5.Generalization.𝔽₃.neg :
      𝔽₃ → 𝔽₃
      Equations
      Instances For
        source
        def IMOSL.IMO2012A5.Generalization.𝔽₃.mul :
        𝔽₃ → 𝔽₃ → 𝔽₃
        Equations
        Instances For
          source
          instance IMOSL.IMO2012A5.Generalization.𝔽₃.instZero :
          Zero 𝔽₃
          Equations
          source
          instance IMOSL.IMO2012A5.Generalization.𝔽₃.instOne :
          One 𝔽₃
          Equations
          source
          instance IMOSL.IMO2012A5.Generalization.𝔽₃.instAdd :
          Add 𝔽₃
          Equations
          source
          instance IMOSL.IMO2012A5.Generalization.𝔽₃.instNeg :
          Neg 𝔽₃
          Equations
          source
          instance IMOSL.IMO2012A5.Generalization.𝔽₃.instMul :
          Mul 𝔽₃
          Equations

          𝔽₃ is a commutative group #

          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.add_zero (x : 𝔽₃) :
          x + 0 = x
          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.zero_add (x : 𝔽₃) :
          0 + x = x
          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.add_comm (x y : 𝔽₃) :
          x + y = y + x
          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.add_assoc (x y z : 𝔽₃) :
          x + y + z = x + (y + z)
          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.neg_add_cancel (x : 𝔽₃) :
          -x + x = 0
          source
          instance IMOSL.IMO2012A5.Generalization.𝔽₃.instAddCommGroup :
          AddCommGroup 𝔽₃
          Equations
          • One or more equations did not get rendered due to their size.

          𝔽₃ is a ring #

          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.zero_mul (x : 𝔽₃) :
          0 * x = 0
          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.mul_zero (x : 𝔽₃) :
          x * 0 = 0
          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.mul_one (x : 𝔽₃) :
          x * 1 = x
          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.one_mul (x : 𝔽₃) :
          1 * x = x
          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.mul_comm (x y : 𝔽₃) :
          x * y = y * x
          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.mul_assoc (x y z : 𝔽₃) :
          x * y * z = x * (y * z)
          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.mul_add (x y z : 𝔽₃) :
          x * (y + z) = x * y + x * z
          source
          theorem IMOSL.IMO2012A5.Generalization.𝔽₃.add_mul (x y z : 𝔽₃) :
          (x + y) * z = x * z + y * z
          source
          instance IMOSL.IMO2012A5.Generalization.𝔽₃.instCommRing :
          CommRing 𝔽₃
          Equations
          • One or more equations did not get rendered due to their size.

          Ring homomorphism from 𝔽₃ #

          source
          def IMOSL.IMO2012A5.Generalization.𝔽₃.cast {R : Type u_1} [AddGroupWithOne R] :
          𝔽₃ → R
          Equations
          Instances For
            source
            theorem IMOSL.IMO2012A5.Generalization.𝔽₃.cast_add {R : Type u_1} [AddGroupWithOne R] (h : 3 = 0) (x y : 𝔽₃) :
            (x + y).cast = x.cast + y.cast
            source
            theorem IMOSL.IMO2012A5.Generalization.𝔽₃.cast_mul {R : Type u_1} [NonAssocRing R] (x y : 𝔽₃) :
            (x * y).cast = x.cast * y.cast
            source
            def IMOSL.IMO2012A5.Generalization.𝔽₃.castRingHom {R : Type u_1} [NonAssocRing R] (h : 3 = 0) :
            𝔽₃ →+* R
            Equations
            Instances For
              source
              theorem IMOSL.IMO2012A5.Generalization.𝔽₃.castRingHom_injective {R : Type u_1} [NonAssocRing R] (h : 3 = 0) (h0 : 1 ≠ 0) :
              Function.Injective ⇑(castRingHom h)