@[simp]

theorem Hex.AlgebraicNumber.ofRat_toComplex (q : ℚ) : (ofRat q).toComplex = ↑q

The executable rational embedding has its expected complex value.

@[simp]

theorem Hex.AlgebraicNumber.one_toComplex : toComplex 1 = 1

Executable one denotes complex one.

theorem Hex.AlgebraicNumber.smul_toComplex (q : ℚ) (a : AlgebraicNumber) : (q • a).toComplex = ↑q * a.toComplex

Executable rational scalar multiplication preserves interpretation.

theorem Hex.AlgebraicNumber.natPow_toComplex (a : AlgebraicNumber) (n : ℕ) : (a.natPow n).toComplex = a.toComplex ^ n

Executable natural powers preserve interpretation.

theorem Hex.AlgebraicNumber.intPow_toComplex (a : AlgebraicNumber) (n : ℤ) : (a.intPow n).toComplex = a.toComplex ^ n

Executable integer powers preserve interpretation.

@[reducible]

noncomputable def Hex.AlgebraicNumber.field : Field AlgebraicNumber

The law-bearing field whose data fields are the executable canonical operations.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.AlgebraicNumber.instField_hexNumberFieldMathlib : Field AlgebraicNumber

Canonical algebraic numbers form a field without replacing any executable arithmetic operation. The instance is computable: every data field is the executable operation, written out, and every law is the corresponding law of field. Code elaborated through the field structure, such as a ^ n resolved by Mathlib's monoid power, therefore compiles and runs.

Equations

• One or more equations did not get rendered due to their size.