## Stream: general

### Topic: Projection is a def, should be lemma

#### Johan Commelin (Oct 04 2019 at 18:00):

#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 (Oct 04 2019 at 18:01):

@Simon Hudon Is this a known issue?

#### Johan Commelin (Oct 04 2019 at 18:07):

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

#### Simon Hudon (Oct 04 2019 at 18:07):

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

Last updated: May 14 2021 at 07:19 UTC