Commit 2023-02-18 18:40 3b6ff86d

View on Github →

feat: port Deprecated.Subring (#2355)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Deprecated/Subring.lean

added theorem IsSubring.inter

added theorem IsSubring.interᵢ

added def IsSubring.subring

added structure IsSubring

added theorem Ring.closure.isSubring

added def Ring.closure

added theorem Ring.closure_mono

added theorem Ring.closure_subset

added theorem Ring.closure_subset_iff

added theorem Ring.exists_list_of_mem_closure

added theorem Ring.image_closure

added theorem Ring.mem_closure

added theorem Ring.subset_closure

added theorem RingHom.isSubring_image

added theorem RingHom.isSubring_preimage

added theorem RingHom.isSubring_set_range

added theorem isSubring_unionᵢ_of_directed