Zulip Chat Archive

Stream: maths

Topic: invalid type ascription

view this post on Zulip Ashvni Narayanan (Aug 28 2020 at 17:27):

import linear_algebra.finite_dimensional
import ring_theory.ideal.basic
import algebra.field
import ring_theory.subring
import ring_theory.integral_closure
import ring_theory.fractional_ideal

class number_field (K : Type*) [field K] :=
(vector_space' : vector_space  K)
(is_algebra' : algebra  K)
(finite_dim : finite_dimensional  K)

variables (K : Type*) [field K] [number_field K]
def ring_of_integers : subring K :=  {}
instance : integral_domain (ring_of_integers : subring K) :=

gives me the error

invalid type ascription, term has type
  Π (K : Type ?) [_inst_1 : field K] [_inst_2 : number_field K], subring K : Type (?+1)
but is expected to have type
  subring K : Type u_1

I don't know how to resolve this. Any help is appreciated, thank you!

view this post on Zulip Reid Barton (Aug 28 2020 at 17:32):

It looks like you just need to say ring_of_integers K (and then you can drop : subring K)

view this post on Zulip Ashvni Narayanan (Aug 28 2020 at 17:34):

Oops, that makes sense, sorry about that. Thank you!

Last updated: May 12 2021 at 08:14 UTC