Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Algebra
Euclidean Domains
ceuf
Next ⟩
df-euf
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
ceuf
Description:
Declare the syntax for the Euclidean function index extractor.
Ref
Expression
Assertion
ceuf
Could not format assertion : No typesetting found for class EuclF with typecode class