@[simp]

theorem Hex.AlgebraicNumber.conj_add (a b : AlgebraicNumber) : (a + b).conj = a.conj + b.conj

@[simp]

theorem Hex.AlgebraicNumber.conj_mul (a b : AlgebraicNumber) : (a * b).conj = a.conj * b.conj

@[simp]

theorem Hex.AlgebraicNumber.conj_eq_self_iff (a : AlgebraicNumber) : a.conj = a ↔ a.isReal = true

@[instance_reducible]

instance Hex.AlgebraicNumber.instStarRing_hexNumberFieldMathlib : StarRing AlgebraicNumber

Equations

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

def Hex.AlgebraicNumber.conjRingEquiv : AlgebraicNumber ≃+* AlgebraicNumber

Conjugation as an involutive field automorphism.

Equations

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

@[simp]

theorem Hex.AlgebraicNumber.conj_neg (a : AlgebraicNumber) : (-a).conj = -a.conj

@[simp]

theorem Hex.AlgebraicNumber.conj_sub (a b : AlgebraicNumber) : (a - b).conj = a.conj - b.conj

@[simp]

theorem Hex.AlgebraicNumber.conj_inv (a : AlgebraicNumber) : a⁻¹.conj = a.conj⁻¹

@[simp]

theorem Hex.AlgebraicNumber.conj_div (a b : AlgebraicNumber) : (a / b).conj = a.conj / b.conj