Projection is a def, should be lemma

Stream: general

[Johan Commelin]

#sanity_check gave me the following complaint:

/- An subring of a Huber ring is called a “ring of integral elements”
if it is open, integrally closed, and power bounded. See [Wedhorn, Def 7.14].-/
structure is_ring_of_integral_elements (Rplus : Type u) (R : Type u)
  [comm_ring Rplus] [topological_space Rplus] [Huber_ring R] [algebra Rplus R]
  extends is_integrally_closed Rplus R, open_embedding (algebra_map R : Rplus → R) : Prop :=
(is_power_bounded : set.range (algebra_map R : Rplus → R) ≤ Rᵒ)

/- INCORRECT DEF/LEMMA: -/
#print is_ring_of_integral_elements.to_is_integrally_closed /- is a def, should be a lemma/theorem -/
#print is_ring_of_integral_elements.to_open_embedding /- is a def, should be a lemma/theorem -/

[Johan Commelin]

@Simon Hudon Is this a known issue?

[Johan Commelin]

@Sebastian Ullrich Just cc-ing you, in case this isn't known.

[Simon Hudon]

I was not involved in writing #sanity_check. I don't know what the policy is with regards to projections