Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Decimal expansion
Division in the extended real number system
cxdiv
Next ⟩
df-xdiv
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
cxdiv
Description:
Extend class notation to include division of extended reals.
Ref
Expression
Assertion
cxdiv
class
÷
𝑒