Metamath Proof Explorer

Syntax definition calgext

Description: Syntax for the algebraic field extension relation.

Ref Expression
Assertion calgext class /AlgExt