bibkey: brauer1950roots
authors: Alfred Brauer
year: 1950
title: "On algebraic equations with all but one root in the interior of the unit circle"
doi: 10.1002/mana.3210040123
url: https://doi.org/10.1002/mana.3210040123
claim: "Bibliographic identification of the classical root-location and irreducibility context; the formal proof is independent."
strata_touched:
  - D5/S0/Tower/DBonacci/Irreducibility
license: citation-only
triage: anchor

Classical multinacci context

The multinacci root-location and irreducibility result is classical. The formalization gives an independent proof from reciprocal monotonicity, complex norm inequalities, the monic constant-product formula and Gauss’s lemma. No theorem from this paper is assumed in Lean.

Crossref metadata identifies Alfred Brauer, Mathematische Nachrichten, volume 4, pages 250-257, with publication year 1950. The primary theorem text and the year printed on the original paper have not been verified. The metadata year is used solely for bibliographic identification.

Verified locator

https://doi.org/10.1002/mana.3210040123

Crossref work record: https://api.crossref.org/works/10.1002/mana.3210040123