Theorems · Theorem · complex analysis

Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv

∀ (p : Polynomial ℚ),
  (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      ((Polynomial.Gal.galActionHom p ℂ)
            ((Polynomial.Gal.restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))).support.card

The number of complex roots equals the number of real roots plus the number of roots not fixed by complex conjugation (i.e. with some imaginary component).

Defined in: Mathlib.Analysis.Complex.Polynomial.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 297 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites49

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

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
Realstatement and proof · cited by 25,697
CommRingproof · cited by 17,173
Finsetproof · cited by 13,712
Algebraproof · cited by 11,388
Set.Elemstatement and proof · cited by 7,166
Polynomialstatement and proof · cited by 5,681
Complexstatement and proof · cited by 5,565
Algebra.algebraMapproof · cited by 4,706
MonoidHomstatement · cited by 3,629
Finset.cardstatement and proof · cited by 2,327

Cited by2

Results whose statement or proof uses this declaration.

Polynomial.Gal.galActionHom_bijective_of_prime_degreeproof · cited by 1
Polynomial.Gal.galActionHom_bijective_of_prime_degree'proof · cited by 0