Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Algebra
Euclidean Domains
ceuf
Next ⟩
df-euf
Metamath Proof Explorer
Unicode
Structured
Syntax definition
ceuf
Description:
Declare the syntax for the Euclidean function index extractor.
Ref
Expression
Assertion
ceuf
class EuclF