record is_riesz_space (K:ordered_field_ch0) (V:pre_riesz_space K) : Prop ≝
{ rs_compat_le_times: ∀a:K.∀f:V. 0≤a → 0≤f → 0≤a*f
record is_riesz_space (K:ordered_field_ch0) (V:pre_riesz_space K) : Prop ≝
{ rs_compat_le_times: ∀a:K.∀f:V. 0≤a → 0≤f → 0≤a*f
definition ring_of_algebra ≝
λK.λA:algebra K.
mk_ring A (a_mult ? A) (a_one ? A)
(a_ring ? ? ? ? (a_algebra_properties ? A)).
definition ring_of_algebra ≝
λK.λA:algebra K.
mk_ring A (a_mult ? A) (a_one ? A)
(a_ring ? ? ? ? (a_algebra_properties ? A)).
record pre_f_algebra (K:ordered_field_ch0) : Type ≝
{ fa_archimedean_riesz_space:> archimedean_riesz_space K;
record pre_f_algebra (K:ordered_field_ch0) : Type ≝
{ fa_archimedean_riesz_space:> archimedean_riesz_space K;
record is_f_algebra (K) (A:pre_f_algebra K) : Prop ≝
{ compat_mult_le: ∀f,g:A.0 ≤ f → 0 ≤ g → 0 ≤ f*g;
record is_f_algebra (K) (A:pre_f_algebra K) : Prop ≝
{ compat_mult_le: ∀f,g:A.0 ≤ f → 0 ≤ g → 0 ≤ f*g;