Definition df-frac

Description: Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025)

	Ref	Expression
Assertion	df-frac	Could not format assertion : No typesetting found for |- Frac = ( r e. _V |-> ( r RLocal ( RLReg ` r ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfrac	Could not format Frac : No typesetting found for class Frac with typecode class
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarr$$
4		crloc	Could not format RLocal : No typesetting found for class RLocal with typecode class
5		crlreg	$$class\mathrm{RLReg}$$
6	3 5	cfv	$$class\mathrm{RLReg}\left(r\right)$$
7	3 6 4	co	Could not format ( r RLocal ( RLReg ` r ) ) : No typesetting found for class ( r RLocal ( RLReg ` r ) ) with typecode class
8	1 2 7	cmpt	Could not format ( r e. _V |-> ( r RLocal ( RLReg ` r ) ) ) : No typesetting found for class ( r e. _V |-> ( r RLocal ( RLReg ` r ) ) ) with typecode class
9	0 8	wceq	Could not format Frac = ( r e. _V |-> ( r RLocal ( RLReg ` r ) ) ) : No typesetting found for wff Frac = ( r e. _V |-> ( r RLocal ( RLReg ` r ) ) ) with typecode wff