WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Exponentiation

Revision #1825 → #2320 · back to history

modifiedPolar form of n th roots of a complex number83e88beba778
FieldFrom #1825To #2320
mathlib.moduleMathlib.RingTheory.Polynomial.BasicMathlib.Algebra.Polynomial.Roots
modifiedOther values of multivalued logarithm and exponentiation93a7085406d1
FieldFrom #1825To #2320
anchor.snippetIfdenotes one of the values of the multivalued logarithm
noteMathlib uses principal values; no multivalued branch enumeration.Mathlib uses principal values; no multivalued branch enumeration. Anchor tightened to disambiguate from other 'If' sentences in this section.
provenanceaiai-moderated
modifiedNumber of values of z^w for rational wa13de209f360
FieldFrom #1825To #2320
anchor.snippetIfis a rational number with m and n coprime integers
noteNo multivalued count lemma in Mathlib.No multivalued count lemma in Mathlib. Anchor tightened to disambiguate from other 'If' sentences in this section.
provenanceaiai-moderated