Lines Matching refs:same
345 and list univ(:'a) =~ univ(:'a) by INFINITE_A_list_BIJ_A (same cardinality)
366 so list univ(:num) =~ univ(:num) by INFINITE_A_list_BIJ_A (same cardinality)
465 INFINITE univ(:'a), which has the same cardinality as univ(:num poly), giving an injection:
1206 (* Overload on finite fields of same cardinality with isomorphic subfields *)
1210 fixity = Infix(NONASSOC, 450), (* same as relation *)
1625 Two finite fields of same cardinality are isomorphic.
1628 (1) Two finite fields of the same cardinality have the same characteristic:
1749 Thus two finite fields with same cardinality are isomorphic.
1870 Given two finite fields r, s of the same cardinality, CARD R = CARD Q.
1917 Two finite fields r and s with the same number of elements CARD R = CARD s.carrier
3238 (3) same as (1)
3265 Let s = ring_bij_image f g r, using the same f.