This is an inofficial mirror of
http://metamath.tirix.org
for personal testing of a visualizer extension only.
Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Decimal expansion
cdp2
Next ⟩
df-dp2
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
cdp2
Description:
Constant used for decimal fraction constructor. See
df-dp2
.
Ref
Expression
Assertion
cdp2
Could not format assertion : No typesetting found for class _ A B with typecode class