Documentation

HexNumberFieldTowerMathlib.Total

source
def Hex.NumberTower.adjoin (T : NumberTower) (a : AlgebraicRoot) :
T.Extension

Adjoin a root to a tower; total by adjoin?_isSome.

Equations
Instances For
    source
    def Hex.NumberTower.factor (T : NumberTower) (f : T.Poly) :
    T.Factorization f

    Factor a polynomial over a tower; total by factor?_isSome.

    Equations
    Instances For
      source
      def Hex.NumberTower.split (T : NumberTower) (f : T.Poly) :
      T.Splitting f

      Split a polynomial over a tower; total by split?_isSome.

      Equations
      Instances For
        source
        def Hex.NumberTower.flatten (T : NumberTower) :
        T.Flattening

        Flatten a tower to a primitive element; total by flatten?_isSome.

        Equations
        Instances For
          source
          @[simp]
          theorem Hex.NumberTower.adjoin?_eq_some (T : NumberTower) (a : AlgebraicRoot) :
          T.adjoin? a = some (T.adjoin a)
          source
          @[simp]
          theorem Hex.NumberTower.factor?_eq_some (T : NumberTower) (f : T.Poly) :
          factor? f = some (T.factor f)
          source
          @[simp]
          theorem Hex.NumberTower.split?_eq_some (T : NumberTower) (f : T.Poly) :
          split? f = some (T.split f)
          source
          @[simp]
          theorem Hex.NumberTower.flatten?_eq_some (T : NumberTower) :
          T.flatten? = some T.flatten