Documentation
HexNumberFieldMathlib
.
Algebraic
Search
return to top
source
Imports
Init
HexNumberFieldMathlib.Embedding
HexNumberFieldMathlib.IntegerRoots
Mathlib.RingTheory.Localization.Integral
Imported by
Hex
.
AlgebraicNumber
.
isAlgebraic
Hex
.
AlgebraicNumber
.
instIsAlgebraicRat_hexNumberFieldMathlib
source
theorem
Hex
.
AlgebraicNumber
.
isAlgebraic
(
a
:
AlgebraicNumber
)
:
IsAlgebraic
ℚ
a
.
toComplex
The represented complex number is algebraic over
ℚ
.
source
instance
Hex
.
AlgebraicNumber
.
instIsAlgebraicRat_hexNumberFieldMathlib
:
Algebra.IsAlgebraic
ℚ
AlgebraicNumber