Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-07 16:29 891c0506

View on Github →

feat(subgroup, subring, subfield): directed Unions of subrings are subrings (#889)

Estimated changes

Modified src/field_theory/subfield.lean

added theorem is_subfield_Union_of_directed

Modified src/group_theory/subgroup.lean

added theorem is_subgroup_Union_of_directed

Modified src/group_theory/submonoid.lean

added theorem is_add_submonoid_Union_of_directed

added theorem is_submonoid_Union_of_directed

Modified src/ring_theory/subring.lean

added theorem is_subring_Union_of_directed