Repository navigation
Complex Infinity #217
Description
Activity
A trade to decide here when this is picked up, from #1394 (comment): since #1396,
Simplifydrops aprovided not d = 0that the answer proves on its own — a quotient byd, a negative power ofd, a logarithm ofd,d^fwithfvanishing, and the indeterminate shapes. With complex infinity,1/dat a zero ofdbecomes a value,∞̃, so the quotient, negative-power and logarithm arms would be dropping a genuine restriction, while the0^0andx/xarms stay right (indeterminate on the sphere too). Eitherprovidedcomes to mean "defined and finite" and the rule stays, or those three arms go with this. Not an argument for or against complex infinity, only a place the two meet.From #1394: the semantics of a
providedbeside a pole follow from here.Simplifynow drops a condition that the answer's ownDomainConditionIn(codomain)already states, so the one decision this issue has to make for that rule is which codomains admit the complex infinity — under those, a quotient's domain condition no longer excludes a zero divisor,1/x provided not x = 0stops being redundant (it has no value at zero where1/xhas an infinite one), and under a codomain without infinities it stays redundant. Signed infinities are already admitted byCCandRRtoday (+oo in CCisTrue), whileln's domain condition still excludes zero, i.e.ln 0 = -oois read as a limit rather than a value; that pair is worth settling here too.- added a commit that references this issue
on Sep 17, 2026 Need to consider how the notation and representation of "directional infinity" is - see #1394 for context
- added a commit that references this issue
on Sep 17, 2026 Part of v3 redesign
Add a complex infinity as multiple times was proposed by @Happypig375