Mathlib Map

Theorems · Theorem · field theory

IsConjRoot.symm

∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x y : A},
  IsConjRoot R x y → IsConjRoot R y x

If y is a conjugate root of x, then x is also a conjugate root of y.

Defined in
Mathlib.FieldTheory.Minpoly.IsConjRoot
Cited by
4 results in Mathlib
Foundations
Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingRingAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

isConjRoot_iff_exists_algEquiv · cited by 2isConjRoot_iff_exists_alg…IsConjRoot.ne_zero_of_injective · cited by 1IsConjRoot.ne_zero_of_inj…IsConjRoot.comm · cited by 0IsConjRoot.commIsConjRoot.isIntegral_iff · cited by 0IsConjRoot.isIntegral_iffCommRing · cited by 17173CommRingAlgebra · cited by 11388AlgebraRing · cited by 7463RingIsConjRoot · cited by 43IsConjRootIsConjRoot.symmCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • CommRingstatement and proof · cited by 17,173
  • Algebrastatement and proof · cited by 11,388
  • Ringstatement and proof · cited by 7,463
  • IsConjRootstatement and proof · cited by 43

Cited by4

Results whose statement or proof uses this declaration.