Lean for "subdomain"

Stream: new members

[Lars Ericson]

What is Lean for "subdomain" in the following statement:

• "A subdomain of an integral domain D is a subset of D which is also an integral domain, for the same operations of addition and multiplication."

Is this translated as is_integral_domain.to_integral_domain ?

I don't know how to express the idea that one type (proof of a set of algebraic properties on some objects) is a subset of another type.

[Johan Commelin]

subring D should work

[Yakov Pechersky]

import ring_theory.subring

variables {D : Type*} [integral_domain D] {SubD : subring D} (hsd : is_integral_domain SubD)

?

[Johan Commelin]

hsd should be automatic by typeclass inference

[Johan Commelin]

every subring of an integral domain is an integral domain

[Yakov Pechersky]

Ah, yes, docs#subring.subring.domain

[Yakov Pechersky]

import ring_theory.subring

variables {R : Type*} [integral_domain R] {D : subring R}

example : integral_domain D := by show_term {apply_instance}
/-
Try this: exact subring.subring.domain D

-/