inline "cic:/CoRN/algebra/CFields/CField.ind".
-coercion "cic:/matita/CoRN-Decl/algebra/CFields/cf_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/algebra/CFields/cf_crr.con 0 (* compounds *).
(* End_SpecReals *)
Implicit Arguments cf_div [F].
*)
+(* NOTATION
+Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80).
+*)
+
(*#*
%\begin{convention}\label{convention:div-form}%
- Division in fields is a (type dependent) ternary function: [(cf_div x y Hy)] is denoted infix by [x [/] y [//] Hy].
Implicit Arguments Frecip [X].
*)
+(* NOTATION
+Notation "{1/} x" := (Frecip x) (at level 2, right associativity).
+*)
+
(* UNEXPORTED
Implicit Arguments Fdiv [X].
*)
+(* NOTATION
+Infix "{/}" := Fdiv (at level 41, no associativity).
+*)
+
(* UNEXPORTED
Hint Resolve included_FRecip included_FDiv : included.
*)