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